defpred S_{1}[ Nat] means for L being Z_Lattice

for l being Linear_Combination of DivisibleMod L

for v being Vector of (DivisibleMod L) st card (Carrier l) = $1 holds

(ScProductDM L) . (v,(Sum l)) = SumSc (v,l);

A1: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A1, A2);

let L be Z_Lattice; :: thesis: for l being Linear_Combination of DivisibleMod L

for v being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

let l be Linear_Combination of DivisibleMod L; :: thesis: for v being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

let v be Vector of (DivisibleMod L); :: thesis: (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

reconsider n = card (Carrier l) as Nat ;

S_{1}[n]
by A3;

hence (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) ; :: thesis: verum

for l being Linear_Combination of DivisibleMod L

for v being Vector of (DivisibleMod L) st card (Carrier l) = $1 holds

(ScProductDM L) . (v,(Sum l)) = SumSc (v,l);

A1: S

proof

A2:
for n being Nat st S
let L be Z_Lattice; :: thesis: for l being Linear_Combination of DivisibleMod L

for v being Vector of (DivisibleMod L) st card (Carrier l) = 0 holds

(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

let l be Linear_Combination of DivisibleMod L; :: thesis: for v being Vector of (DivisibleMod L) st card (Carrier l) = 0 holds

(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

let v be Vector of (DivisibleMod L); :: thesis: ( card (Carrier l) = 0 implies (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) )

assume B1: card (Carrier l) = 0 ; :: thesis: (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

B2: Carrier l = {} by B1;

then Sum l = 0. (DivisibleMod L) by VECTSP_6:19;

then (ScProductDM L) . (v,(Sum l)) = 0. F_Real by ZMODLAT2:14;

hence (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) by B2, LmSumScDM13; :: thesis: verum

end;for v being Vector of (DivisibleMod L) st card (Carrier l) = 0 holds

(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

let l be Linear_Combination of DivisibleMod L; :: thesis: for v being Vector of (DivisibleMod L) st card (Carrier l) = 0 holds

(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

let v be Vector of (DivisibleMod L); :: thesis: ( card (Carrier l) = 0 implies (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) )

assume B1: card (Carrier l) = 0 ; :: thesis: (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

B2: Carrier l = {} by B1;

then Sum l = 0. (DivisibleMod L) by VECTSP_6:19;

then (ScProductDM L) . (v,(Sum l)) = 0. F_Real by ZMODLAT2:14;

hence (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) by B2, LmSumScDM13; :: thesis: verum

S

proof

A3:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume B1: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let L be Z_Lattice; :: thesis: for l being Linear_Combination of DivisibleMod L

for v being Vector of (DivisibleMod L) st card (Carrier l) = n + 1 holds

(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

let l be Linear_Combination of DivisibleMod L; :: thesis: for v being Vector of (DivisibleMod L) st card (Carrier l) = n + 1 holds

(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

let v be Vector of (DivisibleMod L); :: thesis: ( card (Carrier l) = n + 1 implies (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) )

assume B2: card (Carrier l) = n + 1 ; :: thesis: (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

Carrier l <> {} by B2;

then consider u being object such that

B3: u in Carrier l by XBOOLE_0:def 1;

reconsider u = u as Element of (DivisibleMod L) by B3;

B4: card ((Carrier l) \ {u}) = (card (Carrier l)) - (card {u}) by B3, CARD_2:44, ZFMISC_1:31

.= (n + 1) - 1 by B2, CARD_2:42

.= n ;

B5: Carrier l = ((Carrier l) \ {u}) \/ {u} by B3, XBOOLE_1:45, ZFMISC_1:31;

B6: ((Carrier l) \ {u}) /\ {u} = {} by XBOOLE_0:def 7, XBOOLE_1:79;

l is Linear_Combination of Carrier l by VECTSP_6:7;

then consider l1 being Linear_Combination of (Carrier l) \ {u}, l2 being Linear_Combination of {u} such that

B7: l = l1 + l2 by B5, B6, ZMODUL04:26;

Sum l = (Sum l1) + (Sum l2) by B7, ZMODUL02:52;

then B8: (ScProductDM L) . (v,(Sum l)) = ((ScProductDM L) . (v,(Sum l1))) + ((ScProductDM L) . (v,(Sum l2))) by ZMODLAT2:12;

for x being Vector of (DivisibleMod L) st x in (Carrier l) \ {u} holds

x in Carrier l1

then Carrier l1 = (Carrier l) \ {u} by VECTSP_6:def 4;

then B10: (ScProductDM L) . (v,(Sum l1)) = SumSc (v,l1) by B1, B4;

SumSc (v,l2) = (ScProductDM L) . (v,((l2 . u) * u)) by LmSumScDM14

.= (ScProductDM L) . (v,(Sum l2)) by VECTSP_6:17 ;

hence (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) by B7, B8, B10, LmSumScDM1X; :: thesis: verum

end;assume B1: S

let L be Z_Lattice; :: thesis: for l being Linear_Combination of DivisibleMod L

for v being Vector of (DivisibleMod L) st card (Carrier l) = n + 1 holds

(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

let l be Linear_Combination of DivisibleMod L; :: thesis: for v being Vector of (DivisibleMod L) st card (Carrier l) = n + 1 holds

(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

let v be Vector of (DivisibleMod L); :: thesis: ( card (Carrier l) = n + 1 implies (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) )

assume B2: card (Carrier l) = n + 1 ; :: thesis: (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

Carrier l <> {} by B2;

then consider u being object such that

B3: u in Carrier l by XBOOLE_0:def 1;

reconsider u = u as Element of (DivisibleMod L) by B3;

B4: card ((Carrier l) \ {u}) = (card (Carrier l)) - (card {u}) by B3, CARD_2:44, ZFMISC_1:31

.= (n + 1) - 1 by B2, CARD_2:42

.= n ;

B5: Carrier l = ((Carrier l) \ {u}) \/ {u} by B3, XBOOLE_1:45, ZFMISC_1:31;

B6: ((Carrier l) \ {u}) /\ {u} = {} by XBOOLE_0:def 7, XBOOLE_1:79;

l is Linear_Combination of Carrier l by VECTSP_6:7;

then consider l1 being Linear_Combination of (Carrier l) \ {u}, l2 being Linear_Combination of {u} such that

B7: l = l1 + l2 by B5, B6, ZMODUL04:26;

Sum l = (Sum l1) + (Sum l2) by B7, ZMODUL02:52;

then B8: (ScProductDM L) . (v,(Sum l)) = ((ScProductDM L) . (v,(Sum l1))) + ((ScProductDM L) . (v,(Sum l2))) by ZMODLAT2:12;

for x being Vector of (DivisibleMod L) st x in (Carrier l) \ {u} holds

x in Carrier l1

proof

then
(Carrier l) \ {u} c= Carrier l1
;
let x be Vector of (DivisibleMod L); :: thesis: ( x in (Carrier l) \ {u} implies x in Carrier l1 )

assume C1: x in (Carrier l) \ {u} ; :: thesis: x in Carrier l1

x in Carrier l by C1, XBOOLE_0:def 5;

then C2: l . x <> 0. INT.Ring by VECTSP_6:2;

C3: Carrier l2 c= {u} by VECTSP_6:def 4;

C4: l . x = (l1 . x) + (l2 . x) by B7, VECTSP_6:22;

not x in Carrier l2 by C1, C3, XBOOLE_0:def 5;

then l1 . x <> 0. INT.Ring by C2, C4;

hence x in Carrier l1 ; :: thesis: verum

end;assume C1: x in (Carrier l) \ {u} ; :: thesis: x in Carrier l1

x in Carrier l by C1, XBOOLE_0:def 5;

then C2: l . x <> 0. INT.Ring by VECTSP_6:2;

C3: Carrier l2 c= {u} by VECTSP_6:def 4;

C4: l . x = (l1 . x) + (l2 . x) by B7, VECTSP_6:22;

not x in Carrier l2 by C1, C3, XBOOLE_0:def 5;

then l1 . x <> 0. INT.Ring by C2, C4;

hence x in Carrier l1 ; :: thesis: verum

then Carrier l1 = (Carrier l) \ {u} by VECTSP_6:def 4;

then B10: (ScProductDM L) . (v,(Sum l1)) = SumSc (v,l1) by B1, B4;

SumSc (v,l2) = (ScProductDM L) . (v,((l2 . u) * u)) by LmSumScDM14

.= (ScProductDM L) . (v,(Sum l2)) by VECTSP_6:17 ;

hence (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) by B7, B8, B10, LmSumScDM1X; :: thesis: verum

let L be Z_Lattice; :: thesis: for l being Linear_Combination of DivisibleMod L

for v being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

let l be Linear_Combination of DivisibleMod L; :: thesis: for v being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

let v be Vector of (DivisibleMod L); :: thesis: (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)

reconsider n = card (Carrier l) as Nat ;

S

hence (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) ; :: thesis: verum