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 that
A2: u in U and
A3: v in U and
A4: u <> v ; :: thesis: (U \ {u}) \/ {(u + (a * v))} is linearly-independent
set ua = u + (a * v);
set Uu = U \ {u};
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:116; :: thesis: verum

end;

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

now :: thesis: for L being Linear_Combination of (U \ {u}) \/ {(u + (a * v))} st Sum L = 0. V holds
Carrier L = {}

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

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

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

Carrier L c= U \ {u}

proof

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

end;

then reconsider L9 = L as Linear_Combination of U \ {u} by VECTSP_6:def 4;
A11: Sum L9 = 0. V by A6;
U \ {u} is linearly-independent by A1, VECTSP_7:1, XBOOLE_1:36;
hence Carrier L = {} by A11; :: thesis: verum

end;

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

A13: Carrier L c= (U \ {u}) \/ {(u + (a * v))} by VECTSP_6:def 4;
U \ {u} c= U by XBOOLE_1:36;
then (U \ {u}) \/ {(u + (a * v))} c= U \/ {(u + (a * v))} by XBOOLE_1:13;
then A14: Carrier L c= U \/ {(u + (a * v))} by A13;
u + (a * v) in {(u + (a * v))} by TARSKI:def 1;
then u + (a * v) in Lin {(u + (a * v))} by VECTSP_7:8;
then consider Lua being Linear_Combination of {(u + (a * v))} such that
A15: u + (a * v) = Sum Lua by VECTSP_7:7;
reconsider LLua = (L . (u + (a * v))) * Lua as Linear_Combination of {(u + (a * v))} by VECTSP_6:31;
A16: Carrier LLua c= {(u + (a * v))} by VECTSP_6:def 4;
then not u in Carrier LLua by A5, TARSKI:def 1;
then A17: LLua . u = 0. K by VECTSP_6:2;
v in {v} by TARSKI:def 1;
then v in Lin {v} by VECTSP_7:8;
then consider Lv being Linear_Combination of {v} such that
A18: v = Sum Lv by VECTSP_7:7;
reconsider LLv = ((L . (u + (a * v))) * a) * Lv as Linear_Combination of {v} by VECTSP_6:31;
A19: Carrier LLv c= {v} by VECTSP_6:def 4;
then not u in Carrier LLv by A4, TARSKI:def 1;
then A20: LLv . u = 0. K by VECTSP_6:2;
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 3
.= u + (0. V) by VECTSP_1:16
.= u by RLVECT_1:def 4 ;
then u = ((1_ K) * v) + (- (a * v))
.= ((1_ K) * v) + ((- a) * v) by VECTSP_1:21
.= ((1_ K) - a) * v by VECTSP_1:def 15 ;
then A21: {v,u} is linearly-dependent by A4, VECTSP_7:5;
{v,u} c= U by A2, A3, ZFMISC_1:32;
hence contradiction by A1, A21, VECTSP_7:1; :: thesis: verum

end;

then not u + (a * v) in Carrier LLv by A19, TARSKI:def 1;
then A22: LLv . (u + (a * v)) = 0. K by VECTSP_6:2;
A23: u + (a * v) <> 0. V

proof

{v,u} c= U by A2, A3, ZFMISC_1:32;
then A24: {v,u} is linearly-independent by A1, VECTSP_7:1;
A25: (1_ K) * u = u ;
assume 0. V = u + (a * v) ; :: thesis: contradiction
then 1_ K = 0. K by A4, A24, A25, VECTSP_7:6;
hence contradiction ; :: thesis: verum

end;

A26: u <> 0. V by A1, A2, VECTSP_7:2;
(Lua . (u + (a * v))) * (u + (a * v)) = u + (a * v) by A15, VECTSP_6:17
.= (1_ K) * (u + (a * v)) ;
then A27: Lua . (u + (a * v)) = 1_ K by A23, VECTSP10:4;
u in {u} by TARSKI:def 1;
then u in Lin {u} by VECTSP_7:8;
then consider Lu being Linear_Combination of {u} such that
A28: u = Sum Lu by VECTSP_7:7;
reconsider LLu = (L . (u + (a * v))) * Lu as Linear_Combination of {u} by VECTSP_6:31;
A29: Carrier LLu c= {u} by VECTSP_6:def 4;
then not u + (a * v) in Carrier LLu by A5, TARSKI:def 1;
then A30: LLu . (u + (a * v)) = 0. K by VECTSP_6:2;
{u} c= U by A2, ZFMISC_1:31;
then A31: Carrier LLu c= U by A29;
((L + LLv) + LLu) - LLua = (L + (LLv + LLu)) - LLua by VECTSP_6:26
.= (L + (LLv + LLu)) + (- LLua) by VECTSP_6:def 11
.= L + ((LLv + LLu) + (- LLua)) by VECTSP_6:26
.= L + ((LLv + LLu) - LLua) by VECTSP_6:def 11 ;
then A32: Carrier (((L + LLv) + LLu) - LLua) c= (Carrier L) \/ (Carrier ((LLv + LLu) - LLua)) by VECTSP_6:23;
A33: Carrier ((LLv + LLu) - LLua) c= (Carrier (LLv + LLu)) \/ (Carrier LLua) by VECTSP_6:41;
A34: Carrier (LLv + LLu) c= (Carrier LLv) \/ (Carrier LLu) by VECTSP_6:23;
{v} c= U by A3, ZFMISC_1:31;
then Carrier LLv c= U by A19;
then (Carrier LLv) \/ (Carrier LLu) c= U by A31, XBOOLE_1:8;
then Carrier (LLv + LLu) c= U by A34;
then (Carrier (LLv + LLu)) \/ (Carrier LLua) c= U \/ {(u + (a * v))} by A16, XBOOLE_1:13;
then Carrier ((LLv + LLu) - LLua) c= U \/ {(u + (a * v))} by A33;
then (Carrier L) \/ (Carrier ((LLv + LLu) - LLua)) c= U \/ {(u + (a * v))} by A14, XBOOLE_1:8;
then A35: Carrier (((L + LLv) + LLu) - LLua) c= U \/ {(u + (a * v))} by A32;
A36: (((L + LLv) + LLu) - LLua) . (u + (a * v)) = (((L + LLv) + LLu) + (- LLua)) . (u + (a * v)) by VECTSP_6:def 11
.= (((L + LLv) + LLu) . (u + (a * v))) + ((- LLua) . (u + (a * v))) by VECTSP_6:22
.= (((L + LLv) . (u + (a * v))) + (LLu . (u + (a * v)))) + ((- LLua) . (u + (a * v))) by VECTSP_6:22
.= (((L . (u + (a * v))) + (0. K)) + (0. K)) + ((- LLua) . (u + (a * v))) by A22, A30, VECTSP_6:22
.= ((L . (u + (a * v))) + (0. K)) + ((- LLua) . (u + (a * v))) by RLVECT_1:def 4
.= (L . (u + (a * v))) + ((- LLua) . (u + (a * v))) by RLVECT_1:def 4
.= (L . (u + (a * v))) - (LLua . (u + (a * v))) by VECTSP_6:36
.= (L . (u + (a * v))) - ((L . (u + (a * v))) * (1_ K)) by A27, VECTSP_6:def 9
.= (L . (u + (a * v))) - (L . (u + (a * v)))
.= 0. K by VECTSP_1:19 ;
Carrier (((L + LLv) + LLu) - LLua) c= U

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier (((L + LLv) + LLu) - LLua) or x in U )
assume A37: x in Carrier (((L + LLv) + LLu) - LLua) ; :: thesis: x in U
assume not x in U ; :: thesis: contradiction
then A38: x in {(u + (a * v))} by A35, A37, XBOOLE_0:def 3;
ex v being Element of V st
( x = v & (((L + LLv) + LLu) - LLua) . v <> 0. K ) by A37, VECTSP_6:1;
hence contradiction by A36, A38, TARSKI:def 1; :: thesis: verum

end;

then reconsider LLL = ((L + LLv) + LLu) - LLua as Linear_Combination of U by VECTSP_6:def 4;
A39: not u in U \ {u} by ZFMISC_1:56;
not u in {(u + (a * v))} by A5, TARSKI:def 1;
then not u in Carrier L by A13, A39, XBOOLE_0:def 3;
then A40: L . u = 0. K by VECTSP_6:2;
(Lu . u) * u = u by A28, VECTSP_6:17
.= (1_ K) * u ;
then A41: Lu . u = 1_ K by A26, VECTSP10:4;
LLL . u = (((L + LLv) + LLu) + (- LLua)) . u by VECTSP_6:def 11
.= (((L + LLv) + LLu) . u) + ((- LLua) . u) by VECTSP_6:22
.= (((L + LLv) . u) + (LLu . u)) + ((- LLua) . u) by VECTSP_6:22
.= (((L . u) + (LLv . u)) + (LLu . u)) + ((- LLua) . u) by VECTSP_6:22
.= (((0. K) + (0. K)) + (LLu . u)) - (0. K) by A20, A17, A40, VECTSP_6:36
.= ((0. K) + (LLu . u)) - (0. K) by RLVECT_1:def 4
.= (LLu . u) - (0. K) by RLVECT_1:def 4
.= LLu . u by VECTSP_1:18
.= (L . (u + (a * v))) * (1_ K) by A41, VECTSP_6:def 9
.= L . (u + (a * v)) ;
then A42: u in Carrier LLL by A12, VECTSP_6:1;
Sum (((L + LLv) + LLu) - LLua) = (Sum ((L + LLv) + LLu)) - (Sum LLua) by VECTSP_6:47
.= ((Sum (L + LLv)) + (Sum LLu)) - (Sum LLua) by VECTSP_6:44
.= (((Sum L) + (Sum LLv)) + (Sum LLu)) - (Sum LLua) by VECTSP_6:44
.= (((Sum L) + (Sum LLv)) + (Sum LLu)) - ((L . (u + (a * v))) * (u + (a * v))) by A15, VECTSP_6:45
.= (((Sum L) + (Sum LLv)) + ((L . (u + (a * v))) * u)) - ((L . (u + (a * v))) * (u + (a * v))) by A28, VECTSP_6:45
.= (((Sum L) + ((a * (L . (u + (a * v)))) * v)) + ((L . (u + (a * v))) * u)) - ((L . (u + (a * v))) * (u + (a * v))) by A18, VECTSP_6:45
.= (((Sum L) + ((L . (u + (a * v))) * (a * v))) + ((L . (u + (a * v))) * u)) - ((L . (u + (a * v))) * (u + (a * v))) by VECTSP_1:def 16
.= ((Sum L) + (((L . (u + (a * v))) * (a * v)) + ((L . (u + (a * v))) * u))) - ((L . (u + (a * v))) * (u + (a * v))) by RLVECT_1:def 3
.= ((Sum L) + ((L . (u + (a * v))) * ((a * v) + u))) - ((L . (u + (a * v))) * (u + (a * v))) by VECTSP_1:def 14
.= (Sum L) + (((L . (u + (a * v))) * (u + (a * v))) - ((L . (u + (a * v))) * (u + (a * v)))) by RLVECT_1:def 3
.= (0. V) + (0. V) by A6, VECTSP_1:16
.= 0. V by RLVECT_1:def 4 ;
hence Carrier L = {} by A1, A42; :: thesis: verum

end;

end;

end;

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

end;

end;