let V be RealUnitarySpace; :: thesis: for A, B being finite Subset of V

for v being VECTOR of V st v in Lin (A \/ B) & not v in Lin B holds

ex w being VECTOR of V st

( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )

let A, B be finite Subset of V; :: thesis: for v being VECTOR of V st v in Lin (A \/ B) & not v in Lin B holds

ex w being VECTOR of V st

( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )

let v be VECTOR of V; :: thesis: ( v in Lin (A \/ B) & not v in Lin B implies ex w being VECTOR of V st

( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) )

assume that

A1: v in Lin (A \/ B) and

A2: not v in Lin B ; :: thesis: ex w being VECTOR of V st

( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )

consider L being Linear_Combination of A \/ B such that

A3: v = Sum L by A1, RUSUB_3:1;

v in {v} by TARSKI:def 1;

then v in Lin {v} by RUSUB_3:2;

then consider Lv being Linear_Combination of {v} such that

A4: v = Sum Lv by RUSUB_3:1;

A5: Carrier L c= A \/ B by RLVECT_2:def 6;

A9: w in A and

A10: L . w <> 0 ;

consider F being FinSequence of the carrier of V such that

A11: F is one-to-one and

A12: rng F = Carrier L and

A13: Sum L = Sum (L (#) F) by RLVECT_2:def 8;

A14: w in rng F by A10, A12, RLVECT_5:3;

then reconsider Fw1 = F -| w as FinSequence of the carrier of V by FINSEQ_4:41;

reconsider Fw2 = F |-- w as FinSequence of the carrier of V by A14, FINSEQ_4:50;

A15: rng Fw1 misses rng Fw2 by A11, A14, FINSEQ_4:57;

set Fw = Fw1 ^ Fw2;

consider K being Linear_Combination of V such that

A16: Carrier K = (rng (Fw1 ^ Fw2)) /\ (Carrier L) and

A17: L (#) (Fw1 ^ Fw2) = K (#) (Fw1 ^ Fw2) by RLVECT_5:7;

F just_once_values w by A11, A14, FINSEQ_4:8;

then Fw1 ^ Fw2 = F - {w} by FINSEQ_4:54;

then A18: rng (Fw1 ^ Fw2) = (Carrier L) \ {w} by A12, FINSEQ_3:65;

then A19: Carrier K = rng (Fw1 ^ Fw2) by A16, XBOOLE_1:28, XBOOLE_1:36;

then A20: Carrier K c= (A \/ B) \ {w} by A5, A18, XBOOLE_1:33;

take w ; :: thesis: ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )

set a = L . w;

A21: (L . w) " <> 0 by A10, XCMPLX_1:202;

F = ((F -| w) ^ <*w*>) ^ (F |-- w) by A14, FINSEQ_4:51;

then F = Fw1 ^ (<*w*> ^ Fw2) by FINSEQ_1:32;

then L (#) F = (L (#) Fw1) ^ (L (#) (<*w*> ^ Fw2)) by RLVECT_3:34

.= (L (#) Fw1) ^ ((L (#) <*w*>) ^ (L (#) Fw2)) by RLVECT_3:34

.= ((L (#) Fw1) ^ (L (#) <*w*>)) ^ (L (#) Fw2) by FINSEQ_1:32

.= ((L (#) Fw1) ^ <*((L . w) * w)*>) ^ (L (#) Fw2) by RLVECT_2:26 ;

then A22: Sum (L (#) F) = Sum ((L (#) Fw1) ^ (<*((L . w) * w)*> ^ (L (#) Fw2))) by FINSEQ_1:32

.= (Sum (L (#) Fw1)) + (Sum (<*((L . w) * w)*> ^ (L (#) Fw2))) by RLVECT_1:41

.= (Sum (L (#) Fw1)) + ((Sum <*((L . w) * w)*>) + (Sum (L (#) Fw2))) by RLVECT_1:41

.= (Sum (L (#) Fw1)) + ((Sum (L (#) Fw2)) + ((L . w) * w)) by RLVECT_1:44

.= ((Sum (L (#) Fw1)) + (Sum (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:def 3

.= (Sum ((L (#) Fw1) ^ (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:41

.= (Sum (L (#) (Fw1 ^ Fw2))) + ((L . w) * w) by RLVECT_3:34 ;

reconsider K = K as Linear_Combination of (A \/ B) \ {w} by A20, RLVECT_2:def 6;

Carrier ((- K) + Lv) c= (Carrier (- K)) \/ (Carrier Lv) by RLVECT_2:37;

then A23: Carrier ((- K) + Lv) c= (Carrier K) \/ (Carrier Lv) by RLVECT_2:51;

set LC = ((L . w) ") * ((- K) + Lv);

Carrier Lv c= {v} by RLVECT_2:def 6;

then (Carrier K) \/ (Carrier Lv) c= ((A \/ B) \ {w}) \/ {v} by A20, XBOOLE_1:13;

then Carrier ((- K) + Lv) c= ((A \/ B) \ {w}) \/ {v} by A23;

then Carrier (((L . w) ") * ((- K) + Lv)) c= ((A \/ B) \ {w}) \/ {v} by A21, RLVECT_2:42;

then A24: ((L . w) ") * ((- K) + Lv) is Linear_Combination of ((A \/ B) \ {w}) \/ {v} by RLVECT_2:def 6;

( Fw1 is one-to-one & Fw2 is one-to-one ) by A11, A14, FINSEQ_4:52, FINSEQ_4:53;

then Fw1 ^ Fw2 is one-to-one by A15, FINSEQ_3:91;

then Sum (K (#) (Fw1 ^ Fw2)) = Sum K by A19, RLVECT_2:def 8;

then ((L . w) ") * v = (((L . w) ") * (Sum K)) + (((L . w) ") * ((L . w) * w)) by A3, A13, A22, A17, RLVECT_1:def 5

.= (((L . w) ") * (Sum K)) + ((((L . w) ") * (L . w)) * w) by RLVECT_1:def 7

.= (((L . w) ") * (Sum K)) + (1 * w) by A10, XCMPLX_0:def 7

.= (((L . w) ") * (Sum K)) + w by RLVECT_1:def 8 ;

then w = (((L . w) ") * v) - (((L . w) ") * (Sum K)) by RLSUB_2:61

.= ((L . w) ") * (v - (Sum K)) by RLVECT_1:34

.= ((L . w) ") * ((- (Sum K)) + v) by RLVECT_1:def 11 ;

then w = ((L . w) ") * ((Sum (- K)) + (Sum Lv)) by A4, RLVECT_3:3

.= ((L . w) ") * (Sum ((- K) + Lv)) by RLVECT_3:1

.= Sum (((L . w) ") * ((- K) + Lv)) by RLVECT_3:2 ;

hence ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) by A9, A24, RUSUB_3:1; :: thesis: verum

for v being VECTOR of V st v in Lin (A \/ B) & not v in Lin B holds

ex w being VECTOR of V st

( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )

let A, B be finite Subset of V; :: thesis: for v being VECTOR of V st v in Lin (A \/ B) & not v in Lin B holds

ex w being VECTOR of V st

( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )

let v be VECTOR of V; :: thesis: ( v in Lin (A \/ B) & not v in Lin B implies ex w being VECTOR of V st

( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) )

assume that

A1: v in Lin (A \/ B) and

A2: not v in Lin B ; :: thesis: ex w being VECTOR of V st

( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )

consider L being Linear_Combination of A \/ B such that

A3: v = Sum L by A1, RUSUB_3:1;

v in {v} by TARSKI:def 1;

then v in Lin {v} by RUSUB_3:2;

then consider Lv being Linear_Combination of {v} such that

A4: v = Sum Lv by RUSUB_3:1;

A5: Carrier L c= A \/ B by RLVECT_2:def 6;

now :: thesis: ex w being VECTOR of V st

( w in A & not L . w = 0 )

then consider w being VECTOR of V such that ( w in A & not L . w = 0 )

assume A6:
for w being VECTOR of V st w in A holds

L . w = 0 ; :: thesis: contradiction

then Carrier L c= B by A5, XBOOLE_1:73;

then L is Linear_Combination of B by RLVECT_2:def 6;

hence contradiction by A2, A3, RUSUB_3:1; :: thesis: verum

end;L . w = 0 ; :: thesis: contradiction

now :: thesis: for x being object st x in Carrier L holds

not x in A

then
Carrier L misses A
by XBOOLE_0:3;not x in A

let x be object ; :: thesis: ( x in Carrier L implies not x in A )

assume that

A7: x in Carrier L and

A8: x in A ; :: thesis: contradiction

ex u being VECTOR of V st

( x = u & L . u <> 0 ) by A7, RLVECT_5:3;

hence contradiction by A6, A8; :: thesis: verum

end;assume that

A7: x in Carrier L and

A8: x in A ; :: thesis: contradiction

ex u being VECTOR of V st

( x = u & L . u <> 0 ) by A7, RLVECT_5:3;

hence contradiction by A6, A8; :: thesis: verum

then Carrier L c= B by A5, XBOOLE_1:73;

then L is Linear_Combination of B by RLVECT_2:def 6;

hence contradiction by A2, A3, RUSUB_3:1; :: thesis: verum

A9: w in A and

A10: L . w <> 0 ;

consider F being FinSequence of the carrier of V such that

A11: F is one-to-one and

A12: rng F = Carrier L and

A13: Sum L = Sum (L (#) F) by RLVECT_2:def 8;

A14: w in rng F by A10, A12, RLVECT_5:3;

then reconsider Fw1 = F -| w as FinSequence of the carrier of V by FINSEQ_4:41;

reconsider Fw2 = F |-- w as FinSequence of the carrier of V by A14, FINSEQ_4:50;

A15: rng Fw1 misses rng Fw2 by A11, A14, FINSEQ_4:57;

set Fw = Fw1 ^ Fw2;

consider K being Linear_Combination of V such that

A16: Carrier K = (rng (Fw1 ^ Fw2)) /\ (Carrier L) and

A17: L (#) (Fw1 ^ Fw2) = K (#) (Fw1 ^ Fw2) by RLVECT_5:7;

F just_once_values w by A11, A14, FINSEQ_4:8;

then Fw1 ^ Fw2 = F - {w} by FINSEQ_4:54;

then A18: rng (Fw1 ^ Fw2) = (Carrier L) \ {w} by A12, FINSEQ_3:65;

then A19: Carrier K = rng (Fw1 ^ Fw2) by A16, XBOOLE_1:28, XBOOLE_1:36;

then A20: Carrier K c= (A \/ B) \ {w} by A5, A18, XBOOLE_1:33;

take w ; :: thesis: ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )

set a = L . w;

A21: (L . w) " <> 0 by A10, XCMPLX_1:202;

F = ((F -| w) ^ <*w*>) ^ (F |-- w) by A14, FINSEQ_4:51;

then F = Fw1 ^ (<*w*> ^ Fw2) by FINSEQ_1:32;

then L (#) F = (L (#) Fw1) ^ (L (#) (<*w*> ^ Fw2)) by RLVECT_3:34

.= (L (#) Fw1) ^ ((L (#) <*w*>) ^ (L (#) Fw2)) by RLVECT_3:34

.= ((L (#) Fw1) ^ (L (#) <*w*>)) ^ (L (#) Fw2) by FINSEQ_1:32

.= ((L (#) Fw1) ^ <*((L . w) * w)*>) ^ (L (#) Fw2) by RLVECT_2:26 ;

then A22: Sum (L (#) F) = Sum ((L (#) Fw1) ^ (<*((L . w) * w)*> ^ (L (#) Fw2))) by FINSEQ_1:32

.= (Sum (L (#) Fw1)) + (Sum (<*((L . w) * w)*> ^ (L (#) Fw2))) by RLVECT_1:41

.= (Sum (L (#) Fw1)) + ((Sum <*((L . w) * w)*>) + (Sum (L (#) Fw2))) by RLVECT_1:41

.= (Sum (L (#) Fw1)) + ((Sum (L (#) Fw2)) + ((L . w) * w)) by RLVECT_1:44

.= ((Sum (L (#) Fw1)) + (Sum (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:def 3

.= (Sum ((L (#) Fw1) ^ (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:41

.= (Sum (L (#) (Fw1 ^ Fw2))) + ((L . w) * w) by RLVECT_3:34 ;

reconsider K = K as Linear_Combination of (A \/ B) \ {w} by A20, RLVECT_2:def 6;

Carrier ((- K) + Lv) c= (Carrier (- K)) \/ (Carrier Lv) by RLVECT_2:37;

then A23: Carrier ((- K) + Lv) c= (Carrier K) \/ (Carrier Lv) by RLVECT_2:51;

set LC = ((L . w) ") * ((- K) + Lv);

Carrier Lv c= {v} by RLVECT_2:def 6;

then (Carrier K) \/ (Carrier Lv) c= ((A \/ B) \ {w}) \/ {v} by A20, XBOOLE_1:13;

then Carrier ((- K) + Lv) c= ((A \/ B) \ {w}) \/ {v} by A23;

then Carrier (((L . w) ") * ((- K) + Lv)) c= ((A \/ B) \ {w}) \/ {v} by A21, RLVECT_2:42;

then A24: ((L . w) ") * ((- K) + Lv) is Linear_Combination of ((A \/ B) \ {w}) \/ {v} by RLVECT_2:def 6;

( Fw1 is one-to-one & Fw2 is one-to-one ) by A11, A14, FINSEQ_4:52, FINSEQ_4:53;

then Fw1 ^ Fw2 is one-to-one by A15, FINSEQ_3:91;

then Sum (K (#) (Fw1 ^ Fw2)) = Sum K by A19, RLVECT_2:def 8;

then ((L . w) ") * v = (((L . w) ") * (Sum K)) + (((L . w) ") * ((L . w) * w)) by A3, A13, A22, A17, RLVECT_1:def 5

.= (((L . w) ") * (Sum K)) + ((((L . w) ") * (L . w)) * w) by RLVECT_1:def 7

.= (((L . w) ") * (Sum K)) + (1 * w) by A10, XCMPLX_0:def 7

.= (((L . w) ") * (Sum K)) + w by RLVECT_1:def 8 ;

then w = (((L . w) ") * v) - (((L . w) ") * (Sum K)) by RLSUB_2:61

.= ((L . w) ") * (v - (Sum K)) by RLVECT_1:34

.= ((L . w) ") * ((- (Sum K)) + v) by RLVECT_1:def 11 ;

then w = ((L . w) ") * ((Sum (- K)) + (Sum Lv)) by A4, RLVECT_3:3

.= ((L . w) ") * (Sum ((- K) + Lv)) by RLVECT_3:1

.= Sum (((L . w) ") * ((- K) + Lv)) by RLVECT_3:2 ;

hence ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) by A9, A24, RUSUB_3:1; :: thesis: verum