let V be RealLinearSpace; 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; 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; ( 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
; 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, RLVECT_3:14;
A4:
Carrier L c= A \/ B
by RLVECT_2:def 6;
then consider w being VECTOR of V such that
A8:
w in A
and
A9:
L . w <> 0
;
set a = L . w;
take
w
; ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
consider F being FinSequence of the carrier of V such that
A10:
F is one-to-one
and
A11:
rng F = Carrier L
and
A12:
Sum L = Sum (L (#) F)
by RLVECT_2:def 8;
A13:
w in Carrier L
by A9, Th3;
then reconsider Fw1 = F -| w as FinSequence of the carrier of V by A11, FINSEQ_4:41;
reconsider Fw2 = F |-- w as FinSequence of the carrier of V by A11, A13, FINSEQ_4:50;
A14:
rng Fw1 misses rng Fw2
by A10, A11, A13, FINSEQ_4:57;
set Fw = Fw1 ^ Fw2;
F just_once_values w
by A10, A11, A13, FINSEQ_4:8;
then A15:
Fw1 ^ Fw2 = F - {w}
by FINSEQ_4:54;
then A16:
rng (Fw1 ^ Fw2) = (Carrier L) \ {w}
by A11, FINSEQ_3:65;
F = ((F -| w) ^ <*w*>) ^ (F |-- w)
by A11, A13, 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 A17: 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
;
v in {v}
by TARSKI:def 1;
then
v in Lin {v}
by RLVECT_3:15;
then consider Lv being Linear_Combination of {v} such that
A18:
v = Sum Lv
by RLVECT_3:14;
consider K being Linear_Combination of V such that
A19:
Carrier K = (rng (Fw1 ^ Fw2)) /\ (Carrier L)
and
A20:
L (#) (Fw1 ^ Fw2) = K (#) (Fw1 ^ Fw2)
by Th7;
rng (Fw1 ^ Fw2) = (rng F) \ {w}
by A15, FINSEQ_3:65;
then A21:
Carrier K = rng (Fw1 ^ Fw2)
by A11, A19, XBOOLE_1:28;
A22:
(Carrier L) \ {w} c= (A \/ B) \ {w}
by A4, XBOOLE_1:33;
then reconsider K = K as Linear_Combination of (A \/ B) \ {w} by A16, A21, RLVECT_2:def 6;
(L . w) " <> 0
by A9, XCMPLX_1:202;
then A23:
Carrier (((L . w) ") * ((- K) + Lv)) = Carrier ((- K) + Lv)
by RLVECT_2:42;
set LC = ((L . w) ") * ((- K) + Lv);
Carrier ((- K) + Lv) c= (Carrier (- K)) \/ (Carrier Lv)
by RLVECT_2:37;
then A24:
Carrier ((- K) + Lv) c= (Carrier K) \/ (Carrier Lv)
by RLVECT_2:51;
Carrier Lv c= {v}
by RLVECT_2:def 6;
then
(Carrier K) \/ (Carrier Lv) c= ((A \/ B) \ {w}) \/ {v}
by A16, A21, A22, XBOOLE_1:13;
then
Carrier ((- K) + Lv) c= ((A \/ B) \ {w}) \/ {v}
by A24;
then A25:
((L . w) ") * ((- K) + Lv) is Linear_Combination of ((A \/ B) \ {w}) \/ {v}
by A23, RLVECT_2:def 6;
( Fw1 is one-to-one & Fw2 is one-to-one )
by A10, A11, A13, FINSEQ_4:52, FINSEQ_4:53;
then
Fw1 ^ Fw2 is one-to-one
by A14, FINSEQ_3:91;
then
Sum (K (#) (Fw1 ^ Fw2)) = Sum K
by A21, RLVECT_2:def 8;
then ((L . w) ") * v =
(((L . w) ") * (Sum K)) + (((L . w) ") * ((L . w) * w))
by A3, A12, A17, A20, 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 A9, 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 A18, 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 A8, A25, RLVECT_3:14; verum