let V be RealLinearSpace; :: thesis: for A being Subset of V st ( for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ) holds
for p being VECTOR of V st p in A holds
((- p) + A) \ {(0. V)} is linearly-independent
let A be Subset of V; :: thesis: ( ( for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ) implies for p being VECTOR of V st p in A holds
((- p) + A) \ {(0. V)} is linearly-independent )
assume A1: for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ; :: thesis: for p being VECTOR of V st p in A holds
((- p) + A) \ {(0. V)} is linearly-independent
let p be Element of V; :: thesis: ( p in A implies ((- p) + A) \ {(0. V)} is linearly-independent )
assume A2: p in A ; :: thesis: ((- p) + A) \ {(0. V)} is linearly-independent
set pA = (- p) + A;
set pA0 = ((- p) + A) \ {(0. V)};
(- p) + p = 0. V by RLVECT_1:5;
then 0. V in (- p) + A by A2;
then A3: (((- p) + A) \ {(0. V)}) \/ {(0. V)} = (- p) + A by ZFMISC_1:116;
let L be Linear_Combination of ((- p) + A) \ {(0. V)}; :: according to RLVECT_3:def 1 :: thesis: ( not Sum L = 0. V or Carrier L = {} )
assume A4: Sum L = 0. V ; :: thesis: Carrier L = {}
reconsider sL = - (sum L) as Real ;
consider Lp being Linear_Combination of {(0. V)} such that
A5: Lp . (0. V) = sL by RLVECT_4:37;
set LLp = L + Lp;
set pLLp = p + (L + Lp);
A6: Carrier Lp c= {(0. V)} by RLVECT_2:def 6;
A7: p + ((- p) + A) = (p + (- p)) + A by Th5
.= (0. V) + A by RLVECT_1:5
.= A by Th6 ;
A8: Carrier (p + (L + Lp)) = p + (Carrier (L + Lp)) by Th16;
A9: Carrier L c= ((- p) + A) \ {(0. V)} by RLVECT_2:def 6;
then ( Carrier (L + Lp) c= (Carrier L) \/ (Carrier Lp) & (Carrier L) \/ (Carrier Lp) c= (((- p) + A) \ {(0. V)}) \/ {(0. V)} ) by A6, RLVECT_2:37, XBOOLE_1:13;
then Carrier (L + Lp) c= (- p) + A by A3;
then Carrier (p + (L + Lp)) c= A by A7, A8, RLTOPSP1:8;
then A10: p + (L + Lp) is Linear_Combination of A by RLVECT_2:def 6;
A11: sum (p + (L + Lp)) = sum (L + Lp) by Th37;
A12: sum (L + Lp) = (sum L) + (sum Lp) by Th34
.= (sum L) + sL by A5, A6, Th32
.= 0 ;
then Sum (p + (L + Lp)) = (0 * p) + (Sum (L + Lp)) by Th39
.= (0. V) + (Sum (L + Lp)) by RLVECT_1:10
.= Sum (L + Lp)
.= (Sum L) + (Sum Lp) by RLVECT_3:1
.= Sum Lp by A4
.= (Lp . (0. V)) * (0. V) by RLVECT_2:32
.= 0. V ;
then Carrier (p + (L + Lp)) = {} by A1, A10, A11, A12;
then A13: p + (L + Lp) = ZeroLC V by RLVECT_2:def 5;
A14: L + Lp = (0. V) + (L + Lp) by Th21
.= ((- p) + p) + (L + Lp) by RLVECT_1:5
.= (- p) + (ZeroLC V) by A13, Th19
.= ZeroLC V by Th20 ;
assume Carrier L <> {} ; :: thesis: contradiction
then consider v being object such that
A15: v in Carrier L by XBOOLE_0:def 1;
reconsider v = v as Element of V by A15;
not v in Carrier Lp by A6, A9, A15, XBOOLE_0:def 5;
then Lp . v = 0 ;
then (L . v) + 0 = (L + Lp) . v by RLVECT_2:def 10
.= 0 by A14, RLVECT_2:20 ;
hence contradiction by A15, RLVECT_2:19; :: thesis: verum