let V be RealLinearSpace; :: thesis: for A being Subset of V st A is affinely-independent holds

for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {}

let A be Subset of V; :: thesis: ( A is affinely-independent implies for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {} )

assume A1: A is affinely-independent ; :: thesis: for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {}

let L be Linear_Combination of A; :: thesis: ( Sum L = 0. V & sum L = 0 implies Carrier L = {} )

assume that

A2: Sum L = 0. V and

A3: sum L = 0 ; :: thesis: Carrier L = {}

for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {}

let A be Subset of V; :: thesis: ( A is affinely-independent implies for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {} )

assume A1: A is affinely-independent ; :: thesis: for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {}

let L be Linear_Combination of A; :: thesis: ( Sum L = 0. V & sum L = 0 implies Carrier L = {} )

assume that

A2: Sum L = 0. V and

A3: sum L = 0 ; :: thesis: Carrier L = {}

per cases
( A is empty or not A is empty )
;

end;

suppose
not A is empty
; :: thesis: Carrier L = {}

then consider p being VECTOR of V such that

A4: p in A and

A5: ((- p) + A) \ {(0. V)} is linearly-independent by A1;

A6: A \/ {p} = A by A4, ZFMISC_1:40;

consider Lp being Linear_Combination of {p} such that

A7: Lp . p = L . p by RLVECT_4:37;

set LLp = L - Lp;

((- p) + (L - Lp)) . (0. V) = (L - Lp) . ((0. V) - (- p)) by Def1

.= (L - Lp) . (- (- p)) by RLVECT_1:14

.= (L - Lp) . p

.= (L . p) - (Lp . p) by RLVECT_2:54

.= 0 by A7 ;

then A8: not 0. V in Carrier ((- p) + (L - Lp)) by RLVECT_2:19;

A9: Carrier Lp c= {p} by RLVECT_2:def 6;

then A10: ( Carrier Lp = {p} or Carrier Lp = {} ) by ZFMISC_1:33;

Carrier L c= A by RLVECT_2:def 6;

then ( Carrier (L - Lp) c= (Carrier L) \/ (Carrier Lp) & (Carrier L) \/ (Carrier Lp) c= A \/ {p} ) by A9, RLVECT_2:55, XBOOLE_1:13;

then A11: Carrier (L - Lp) c= A by A6;

Carrier ((- p) + (L - Lp)) = (- p) + (Carrier (L - Lp)) by Th16;

then Carrier ((- p) + (L - Lp)) c= (- p) + A by A11, RLTOPSP1:8;

then Carrier ((- p) + (L - Lp)) c= ((- p) + A) \ {(0. V)} by A8, ZFMISC_1:34;

then A12: (- p) + (L - Lp) is Linear_Combination of ((- p) + A) \ {(0. V)} by RLVECT_2:def 6;

A13: (L - Lp) + Lp = L + (Lp - Lp) by RLVECT_2:40

.= L + (ZeroLC V) by RLVECT_2:57

.= L by RLVECT_2:41 ;

A14: Sum ((- p) + Lp) = ((sum Lp) * (- p)) + (Sum Lp) by Th39

.= ((sum Lp) * (- p)) + ((Lp . p) * p) by RLVECT_2:32

.= ((Lp . p) * (- p)) + ((Lp . p) * p) by A9, Th32

.= (Lp . p) * ((- p) + p) by RLVECT_1:def 5

.= (Lp . p) * (0. V) by RLVECT_1:5

.= 0. V ;

Sum ((- p) + L) = ((sum L) * (- p)) + (Sum L) by Th39

.= (0. V) + (0. V) by A2, A3, RLVECT_1:10

.= 0. V ;

then 0. V = Sum (((- p) + (L - Lp)) + ((- p) + Lp)) by A13, Th17

.= (Sum ((- p) + (L - Lp))) + (0. V) by A14, RLVECT_3:1

.= Sum ((- p) + (L - Lp)) ;

then {} = Carrier ((- p) + (L - Lp)) by A5, A12;

then A15: ZeroLC V = (- p) + (L - Lp) by RLVECT_2:def 5;

A16: L - Lp = (0. V) + (L - Lp) by Th21

.= (p + (- p)) + (L - Lp) by RLVECT_1:5

.= p + ((- p) + (L - Lp)) by Th19

.= ZeroLC V by A15, Th20 ;

then sum (L - Lp) = 0 by Th31;

then 0 = 0 + (sum Lp) by A3, A13, Th34

.= 0 + (Lp . p) by A9, Th32 ;

then not p in Carrier Lp by RLVECT_2:19;

then (Carrier (L - Lp)) \/ (Carrier Lp) = {} by A10, A16, RLVECT_2:def 5, TARSKI:def 1;

then Carrier L c= {} by A13, RLVECT_2:37;

hence Carrier L = {} ; :: thesis: verum

end;A4: p in A and

A5: ((- p) + A) \ {(0. V)} is linearly-independent by A1;

A6: A \/ {p} = A by A4, ZFMISC_1:40;

consider Lp being Linear_Combination of {p} such that

A7: Lp . p = L . p by RLVECT_4:37;

set LLp = L - Lp;

((- p) + (L - Lp)) . (0. V) = (L - Lp) . ((0. V) - (- p)) by Def1

.= (L - Lp) . (- (- p)) by RLVECT_1:14

.= (L - Lp) . p

.= (L . p) - (Lp . p) by RLVECT_2:54

.= 0 by A7 ;

then A8: not 0. V in Carrier ((- p) + (L - Lp)) by RLVECT_2:19;

A9: Carrier Lp c= {p} by RLVECT_2:def 6;

then A10: ( Carrier Lp = {p} or Carrier Lp = {} ) by ZFMISC_1:33;

Carrier L c= A by RLVECT_2:def 6;

then ( Carrier (L - Lp) c= (Carrier L) \/ (Carrier Lp) & (Carrier L) \/ (Carrier Lp) c= A \/ {p} ) by A9, RLVECT_2:55, XBOOLE_1:13;

then A11: Carrier (L - Lp) c= A by A6;

Carrier ((- p) + (L - Lp)) = (- p) + (Carrier (L - Lp)) by Th16;

then Carrier ((- p) + (L - Lp)) c= (- p) + A by A11, RLTOPSP1:8;

then Carrier ((- p) + (L - Lp)) c= ((- p) + A) \ {(0. V)} by A8, ZFMISC_1:34;

then A12: (- p) + (L - Lp) is Linear_Combination of ((- p) + A) \ {(0. V)} by RLVECT_2:def 6;

A13: (L - Lp) + Lp = L + (Lp - Lp) by RLVECT_2:40

.= L + (ZeroLC V) by RLVECT_2:57

.= L by RLVECT_2:41 ;

A14: Sum ((- p) + Lp) = ((sum Lp) * (- p)) + (Sum Lp) by Th39

.= ((sum Lp) * (- p)) + ((Lp . p) * p) by RLVECT_2:32

.= ((Lp . p) * (- p)) + ((Lp . p) * p) by A9, Th32

.= (Lp . p) * ((- p) + p) by RLVECT_1:def 5

.= (Lp . p) * (0. V) by RLVECT_1:5

.= 0. V ;

Sum ((- p) + L) = ((sum L) * (- p)) + (Sum L) by Th39

.= (0. V) + (0. V) by A2, A3, RLVECT_1:10

.= 0. V ;

then 0. V = Sum (((- p) + (L - Lp)) + ((- p) + Lp)) by A13, Th17

.= (Sum ((- p) + (L - Lp))) + (0. V) by A14, RLVECT_3:1

.= Sum ((- p) + (L - Lp)) ;

then {} = Carrier ((- p) + (L - Lp)) by A5, A12;

then A15: ZeroLC V = (- p) + (L - Lp) by RLVECT_2:def 5;

A16: L - Lp = (0. V) + (L - Lp) by Th21

.= (p + (- p)) + (L - Lp) by RLVECT_1:5

.= p + ((- p) + (L - Lp)) by Th19

.= ZeroLC V by A15, Th20 ;

then sum (L - Lp) = 0 by Th31;

then 0 = 0 + (sum Lp) by A3, A13, Th34

.= 0 + (Lp . p) by A9, Th32 ;

then not p in Carrier Lp by RLVECT_2:19;

then (Carrier (L - Lp)) \/ (Carrier Lp) = {} by A10, A16, RLVECT_2:def 5, TARSKI:def 1;

then Carrier L c= {} by A13, RLVECT_2:37;

hence Carrier L = {} ; :: thesis: verum