let V be Z_Module; :: thesis: for L being Linear_Combination of V

for F being FinSequence of V st Carrier L misses rng F holds

Sum (L (#) F) = 0. V

let L be Linear_Combination of V; :: thesis: for F being FinSequence of V st Carrier L misses rng F holds

Sum (L (#) F) = 0. V

defpred S_{1}[ FinSequence] means for G being FinSequence of V st G = $1 & Carrier L misses rng G holds

Sum (L (#) G) = 0. V;

A1: for p being FinSequence

for x being object st S_{1}[p] holds

S_{1}[p ^ <*x*>]
_{1}[ {} ]
_{1}[p]
from FINSEQ_1:sch 3(A10, A1);

let F be FinSequence of V; :: thesis: ( Carrier L misses rng F implies Sum (L (#) F) = 0. V )

assume Carrier L misses rng F ; :: thesis: Sum (L (#) F) = 0. V

hence Sum (L (#) F) = 0. V by A12; :: thesis: verum

for F being FinSequence of V st Carrier L misses rng F holds

Sum (L (#) F) = 0. V

let L be Linear_Combination of V; :: thesis: for F being FinSequence of V st Carrier L misses rng F holds

Sum (L (#) F) = 0. V

defpred S

Sum (L (#) G) = 0. V;

A1: for p being FinSequence

for x being object st S

S

proof

A10:
S
let p be FinSequence; :: thesis: for x being object st S_{1}[p] holds

S_{1}[p ^ <*x*>]

let x be object ; :: thesis: ( S_{1}[p] implies S_{1}[p ^ <*x*>] )

assume A2: S_{1}[p]
; :: thesis: S_{1}[p ^ <*x*>]

let G be FinSequence of V; :: thesis: ( G = p ^ <*x*> & Carrier L misses rng G implies Sum (L (#) G) = 0. V )

assume A3: G = p ^ <*x*> ; :: thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V )

then reconsider p = p, x9 = <*x*> as FinSequence of V by FINSEQ_1:36;

x in {x} by TARSKI:def 1;

then A4: x in rng x9 by FINSEQ_1:38;

reconsider x = x as Vector of V by A4;

assume Carrier L misses rng G ; :: thesis: Sum (L (#) G) = 0. V

then A5: {} = (Carrier L) /\ (rng G) by XBOOLE_0:def 7

.= (Carrier L) /\ ((rng p) \/ (rng <*x*>)) by A3, FINSEQ_1:31

.= (Carrier L) /\ ((rng p) \/ {x}) by FINSEQ_1:38

.= ((Carrier L) /\ (rng p)) \/ ((Carrier L) /\ {x}) by XBOOLE_1:23 ;

then (Carrier L) /\ (rng p) = {} ;

then A6: Sum (L (#) p) = 0. V by A2, XBOOLE_0:def 7;

A7: (Carrier L) /\ {x} = {} by A5;

Sum (L (#) G) = Sum ((L (#) p) ^ (L (#) x9)) by A3, ZMODUL02:51

.= (Sum (L (#) p)) + (Sum (L (#) x9)) by RLVECT_1:41

.= (0. V) + (Sum <*((L . x) * x)*>) by A6, ZMODUL02:15

.= Sum <*((L . x) * x)*> by RLVECT_1:4

.= (0. INT.Ring) * x by A9, RLVECT_1:44

.= 0. V by ZMODUL01:1 ;

hence Sum (L (#) G) = 0. V ; :: thesis: verum

end;S

let x be object ; :: thesis: ( S

assume A2: S

let G be FinSequence of V; :: thesis: ( G = p ^ <*x*> & Carrier L misses rng G implies Sum (L (#) G) = 0. V )

assume A3: G = p ^ <*x*> ; :: thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V )

then reconsider p = p, x9 = <*x*> as FinSequence of V by FINSEQ_1:36;

x in {x} by TARSKI:def 1;

then A4: x in rng x9 by FINSEQ_1:38;

reconsider x = x as Vector of V by A4;

assume Carrier L misses rng G ; :: thesis: Sum (L (#) G) = 0. V

then A5: {} = (Carrier L) /\ (rng G) by XBOOLE_0:def 7

.= (Carrier L) /\ ((rng p) \/ (rng <*x*>)) by A3, FINSEQ_1:31

.= (Carrier L) /\ ((rng p) \/ {x}) by FINSEQ_1:38

.= ((Carrier L) /\ (rng p)) \/ ((Carrier L) /\ {x}) by XBOOLE_1:23 ;

then (Carrier L) /\ (rng p) = {} ;

then A6: Sum (L (#) p) = 0. V by A2, XBOOLE_0:def 7;

A7: (Carrier L) /\ {x} = {} by A5;

now :: thesis: not x in Carrier L

then A9:
L . x = 0
;A8:
x in {x}
by TARSKI:def 1;

assume x in Carrier L ; :: thesis: contradiction

hence contradiction by A7, A8, XBOOLE_0:def 4; :: thesis: verum

end;assume x in Carrier L ; :: thesis: contradiction

hence contradiction by A7, A8, XBOOLE_0:def 4; :: thesis: verum

Sum (L (#) G) = Sum ((L (#) p) ^ (L (#) x9)) by A3, ZMODUL02:51

.= (Sum (L (#) p)) + (Sum (L (#) x9)) by RLVECT_1:41

.= (0. V) + (Sum <*((L . x) * x)*>) by A6, ZMODUL02:15

.= Sum <*((L . x) * x)*> by RLVECT_1:4

.= (0. INT.Ring) * x by A9, RLVECT_1:44

.= 0. V by ZMODUL01:1 ;

hence Sum (L (#) G) = 0. V ; :: thesis: verum

proof

A12:
for p being FinSequence holds S
let G be FinSequence of V; :: thesis: ( G = {} & Carrier L misses rng G implies Sum (L (#) G) = 0. V )

assume G = {} ; :: thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V )

then A11: L (#) G = <*> the carrier of V by ZMODUL02:14;

assume Carrier L misses rng G ; :: thesis: Sum (L (#) G) = 0. V

thus Sum (L (#) G) = 0. V by A11, RLVECT_1:43; :: thesis: verum

end;assume G = {} ; :: thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V )

then A11: L (#) G = <*> the carrier of V by ZMODUL02:14;

assume Carrier L misses rng G ; :: thesis: Sum (L (#) G) = 0. V

thus Sum (L (#) G) = 0. V by A11, RLVECT_1:43; :: thesis: verum

let F be FinSequence of V; :: thesis: ( Carrier L misses rng F implies Sum (L (#) F) = 0. V )

assume Carrier L misses rng F ; :: thesis: Sum (L (#) F) = 0. V

hence Sum (L (#) F) = 0. V by A12; :: thesis: verum