let K be Field; :: thesis: for a being Element of K
for V being VectSp of K
for U being finite Subset of V st U is linearly-independent holds
for u, v being Vector of V st u in U & v in U & u <> v holds
(U \ {u}) \/ {(u + (a * v))} is linearly-independent
let a be Element of K; :: thesis: for V being VectSp of K
for U being finite Subset of V st U is linearly-independent holds
for u, v being Vector of V st u in U & v in U & u <> v holds
(U \ {u}) \/ {(u + (a * v))} is linearly-independent
let V be VectSp of K; :: thesis: for U being finite Subset of V st U is linearly-independent holds
for u, v being Vector of V st u in U & v in U & u <> v holds
(U \ {u}) \/ {(u + (a * v))} is linearly-independent
let U be finite Subset of V; :: thesis: ( U is linearly-independent implies for u, v being Vector of V st u in U & v in U & u <> v holds
(U \ {u}) \/ {(u + (a * v))} is linearly-independent )
assume A1: U is linearly-independent ; :: thesis: for u, v being Vector of V st u in U & v in U & u <> v holds
(U \ {u}) \/ {(u + (a * v))} is linearly-independent
let u, v be Vector of V; :: thesis: ( u in U & v in U & u <> v implies (U \ {u}) \/ {(u + (a * v))} is linearly-independent )
assume A2: ( u in U & v in U & u <> v ) ; :: thesis: (U \ {u}) \/ {(u + (a * v))} is linearly-independent
set Uu = U \ {u};
set ua = u + (a * v);
set Uua = (U \ {u}) \/ {(u + (a * v))};

per cases ( u = u + (a * v) or u <> u + (a * v) ) ;

suppose u = u + (a * v) ; :: thesis: (U \ {u}) \/ {(u + (a * v))} is linearly-independent

hence (U \ {u}) \/ {(u + (a * v))} is linearly-independent by A1, A2, ZFMISC_1:140; :: thesis: verum

end;

suppose A3: u <> u + (a * v) ; :: thesis: (U \ {u}) \/ {(u + (a * v))} is linearly-independent

now

let L be Linear_Combination of (U \ {u}) \/ {(u + (a * v))}; :: thesis: ( Sum L = 0. V implies Carrier b₁ = {} )
assume A4: Sum L = 0. V ; :: thesis: Carrier b₁ = {}

per cases ( L . (u + (a * v)) = 0. K or L . (u + (a * v)) <> 0. K ) ;

suppose A5: L . (u + (a * v)) = 0. K ; :: thesis: Carrier b₁ = {}

Carrier L c= U \ {u}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier L or x in U \ {u} )
assume A6: x in Carrier L ; :: thesis: x in U \ {u}
then consider v being Vector of V such that
A7: ( x = v & L . v <> 0. K ) by VECTSP_6:19;
Carrier L c= (U \ {u}) \/ {(u + (a * v))} by VECTSP_6:def 7;
then ( v in U \ {u} or ( v in {(u + (a * v))} & not v in {(u + (a * v))} ) ) by A5, A6, A7, TARSKI:def 1, XBOOLE_0:def 3;
hence x in U \ {u} by A7; :: thesis: verum

end;

then reconsider L' = L as Linear_Combination of U \ {u} by VECTSP_6:def 7;
( U \ {u} is linearly-independent & Sum L' = 0. V ) by A1, A4, VECTSP_7:2, XBOOLE_1:36;
hence Carrier L = {} by VECTSP_7:def 1; :: thesis: verum

end;

suppose A8: L . (u + (a * v)) <> 0. K ; :: thesis: Carrier b₁ = {}

( u + (a * v) in {(u + (a * v))} & u in {u} & v in {v} ) by TARSKI:def 1;
then A9: ( u + (a * v) in Lin {(u + (a * v))} & u in Lin {u} & v in Lin {v} ) by VECTSP_7:13;
then consider Lua being Linear_Combination of {(u + (a * v))} such that
A10: u + (a * v) = Sum Lua by VECTSP_7:12;
consider Lu being Linear_Combination of {u} such that
A11: u = Sum Lu by A9, VECTSP_7:12;
consider Lv being Linear_Combination of {v} such that
A12: v = Sum Lv by A9, VECTSP_7:12;
reconsider LLua = (L . (u + (a * v))) * Lua as Linear_Combination of {(u + (a * v))} by VECTSP_6:61;
reconsider LLv = ((L . (u + (a * v))) * a) * Lv as Linear_Combination of {v} by VECTSP_6:61;
reconsider LLu = (L . (u + (a * v))) * Lu as Linear_Combination of {u} by VECTSP_6:61;
A13: Sum (((L + LLv) + LLu) - LLua) = (Sum ((L + LLv) + LLu)) - (Sum LLua) by VECTSP_6:80
.= ((Sum (L + LLv)) + (Sum LLu)) - (Sum LLua) by VECTSP_6:77
.= (((Sum L) + (Sum LLv)) + (Sum LLu)) - (Sum LLua) by VECTSP_6:77
.= (((Sum L) + (Sum LLv)) + (Sum LLu)) - ((L . (u + (a * v))) * (u + (a * v))) by A10, VECTSP_6:78
.= (((Sum L) + (Sum LLv)) + ((L . (u + (a * v))) * u)) - ((L . (u + (a * v))) * (u + (a * v))) by A11, VECTSP_6:78
.= (((Sum L) + ((a * (L . (u + (a * v)))) * v)) + ((L . (u + (a * v))) * u)) - ((L . (u + (a * v))) * (u + (a * v))) by A12, VECTSP_6:78
.= (((Sum L) + ((L . (u + (a * v))) * (a * v))) + ((L . (u + (a * v))) * u)) - ((L . (u + (a * v))) * (u + (a * v))) by VECTSP_1:def 26
.= ((Sum L) + (((L . (u + (a * v))) * (a * v)) + ((L . (u + (a * v))) * u))) - ((L . (u + (a * v))) * (u + (a * v))) by RLVECT_1:def 6
.= ((Sum L) + ((L . (u + (a * v))) * ((a * v) + u))) - ((L . (u + (a * v))) * (u + (a * v))) by VECTSP_1:def 26
.= (Sum L) + (((L . (u + (a * v))) * (u + (a * v))) - ((L . (u + (a * v))) * (u + (a * v)))) by RLVECT_1:def 6
.= (0. V) + (0. V) by A4, VECTSP_1:63
.= 0. V by RLVECT_1:def 7 ;
A14: ( Carrier LLv c= {v} & {v} c= U & Carrier LLu c= {u} & {u} c= U & Carrier LLua c= {(u + (a * v))} & Carrier L c= (U \ {u}) \/ {(u + (a * v))} ) by A2, VECTSP_6:def 7, ZFMISC_1:37;
then ( Carrier LLv c= U & Carrier LLu c= U ) by XBOOLE_1:1;
then ( Carrier (LLv + LLu) c= (Carrier LLv) \/ (Carrier LLu) & (Carrier LLv) \/ (Carrier LLu) c= U ) by VECTSP_6:51, XBOOLE_1:8;
then ( Carrier (LLv + LLu) c= U & U \ {u} c= U ) by XBOOLE_1:1, XBOOLE_1:36;
then ( (Carrier (LLv + LLu)) \/ (Carrier LLua) c= U \/ {(u + (a * v))} & (U \ {u}) \/ {(u + (a * v))} c= U \/ {(u + (a * v))} & Carrier ((LLv + LLu) - LLua) c= (Carrier (LLv + LLu)) \/ (Carrier LLua) ) by A14, VECTSP_6:74, XBOOLE_1:13;
then A15: ( Carrier ((LLv + LLu) - LLua) c= U \/ {(u + (a * v))} & Carrier L c= U \/ {(u + (a * v))} ) by A14, XBOOLE_1:1;
((L + LLv) + LLu) - LLua = (L + (LLv + LLu)) - LLua by VECTSP_6:54
.= (L + (LLv + LLu)) + (- LLua) by VECTSP_6:def 14
.= L + ((LLv + LLu) + (- LLua)) by VECTSP_6:54
.= L + ((LLv + LLu) - LLua) by VECTSP_6:def 14 ;
then ( Carrier (((L + LLv) + LLu) - LLua) c= (Carrier L) \/ (Carrier ((LLv + LLu) - LLua)) & (Carrier L) \/ (Carrier ((LLv + LLu) - LLua)) c= U \/ {(u + (a * v))} ) by A15, VECTSP_6:51, XBOOLE_1:8;
then A16: Carrier (((L + LLv) + LLu) - LLua) c= U \/ {(u + (a * v))} by XBOOLE_1:1;
v <> u + (a * v)

proof

assume v = u + (a * v) ; :: thesis: contradiction
then v - (a * v) = u + ((a * v) - (a * v)) by RLVECT_1:def 6
.= u + (0. V) by VECTSP_1:63
.= u by RLVECT_1:def 7 ;
then u = ((1_ K) * v) + (- (a * v)) by VECTSP_1:def 26
.= ((1_ K) * v) + ((- a) * v) by VECTSP_1:68
.= ((1_ K) - a) * v by VECTSP_1:def 26 ;
then A17: not {v,u} is linearly-independent by A2, VECTSP_7:8;
{v,u} c= U by A2, ZFMISC_1:38;
hence contradiction by A1, A17, VECTSP_7:2; :: thesis: verum

end;

then ( not u + (a * v) in Carrier LLv & not u + (a * v) in Carrier LLu ) by A3, A14, TARSKI:def 1;
then A18: ( LLv . (u + (a * v)) = 0. K & LLu . (u + (a * v)) = 0. K ) by VECTSP_6:20;
A19: u + (a * v) <> 0. V

proof

assume A20: 0. V = u + (a * v) ; :: thesis: contradiction
{v,u} c= U by A2, ZFMISC_1:38;
then ( {v,u} is linearly-independent & (1_ K) * u = u ) by A1, VECTSP_1:def 26, VECTSP_7:2;
then 1_ K = 0. K by A2, A20, VECTSP_7:9;
hence contradiction ; :: thesis: verum

end;

(Lua . (u + (a * v))) * (u + (a * v)) = u + (a * v) by A10, VECTSP_6:43
.= (1_ K) * (u + (a * v)) by VECTSP_1:def 26 ;
then A21: Lua . (u + (a * v)) = 1_ K by A19, VECTSP10:5;
A22: (((L + LLv) + LLu) - LLua) . (u + (a * v)) = (((L + LLv) + LLu) + (- LLua)) . (u + (a * v)) by VECTSP_6:def 14
.= (((L + LLv) + LLu) . (u + (a * v))) + ((- LLua) . (u + (a * v))) by VECTSP_6:def 11
.= (((L + LLv) . (u + (a * v))) + (LLu . (u + (a * v)))) + ((- LLua) . (u + (a * v))) by VECTSP_6:def 11
.= (((L . (u + (a * v))) + (0. K)) + (0. K)) + ((- LLua) . (u + (a * v))) by A18, VECTSP_6:def 11
.= ((L . (u + (a * v))) + (0. K)) + ((- LLua) . (u + (a * v))) by RLVECT_1:def 7
.= (L . (u + (a * v))) + ((- LLua) . (u + (a * v))) by RLVECT_1:def 7
.= (L . (u + (a * v))) - (LLua . (u + (a * v))) by VECTSP_6:67
.= (L . (u + (a * v))) - ((L . (u + (a * v))) * (1_ K)) by A21, VECTSP_6:def 12
.= (L . (u + (a * v))) - (L . (u + (a * v))) by VECTSP_1:def 13
.= 0. K by VECTSP_1:66 ;
Carrier (((L + LLv) + LLu) - LLua) c= U

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier (((L + LLv) + LLu) - LLua) or x in U )
assume A23: x in Carrier (((L + LLv) + LLu) - LLua) ; :: thesis: x in U
then consider v being Element of V such that
A24: ( x = v & (((L + LLv) + LLu) - LLua) . v <> 0. K ) by VECTSP_6:19;
assume not x in U ; :: thesis: contradiction
then x in {(u + (a * v))} by A16, A23, XBOOLE_0:def 3;
hence contradiction by A22, A24, TARSKI:def 1; :: thesis: verum

end;

then reconsider LLL = ((L + LLv) + LLu) - LLua as Linear_Combination of U by VECTSP_6:def 7;
( not u in {(u + (a * v))} & not u in U \ {u} ) by A3, TARSKI:def 1, ZFMISC_1:64;
then ( not u in Carrier LLv & not u in Carrier LLua & not u in Carrier L ) by A2, A14, TARSKI:def 1, XBOOLE_0:def 3;
then A25: ( LLv . u = 0. K & LLua . u = 0. K & L . u = 0. K ) by VECTSP_6:20;
A26: u <> 0. V by A1, A2, VECTSP_7:3;
(Lu . u) * u = u by A11, VECTSP_6:43
.= (1_ K) * u by VECTSP_1:def 26 ;
then A27: Lu . u = 1_ K by A26, VECTSP10:5;
LLL . u = (((L + LLv) + LLu) + (- LLua)) . u by VECTSP_6:def 14
.= (((L + LLv) + LLu) . u) + ((- LLua) . u) by VECTSP_6:def 11
.= (((L + LLv) . u) + (LLu . u)) + ((- LLua) . u) by VECTSP_6:def 11
.= (((L . u) + (LLv . u)) + (LLu . u)) + ((- LLua) . u) by VECTSP_6:def 11
.= (((0. K) + (0. K)) + (LLu . u)) - (0. K) by A25, VECTSP_6:67
.= ((0. K) + (LLu . u)) - (0. K) by RLVECT_1:def 7
.= (LLu . u) - (0. K) by RLVECT_1:def 7
.= LLu . u by VECTSP_1:65
.= (L . (u + (a * v))) * (1_ K) by A27, VECTSP_6:def 12
.= L . (u + (a * v)) by VECTSP_1:def 13 ;
then u in Carrier LLL by A8, VECTSP_6:19;
hence Carrier L = {} by A1, A13, VECTSP_7:def 1; :: thesis: verum

end;

end;

end;

hence (U \ {u}) \/ {(u + (a * v))} is linearly-independent by VECTSP_7:def 1; :: thesis: verum

end;

end;