let K be Field; :: thesis: for V being VectSp of K
for U being finite Subset of V
for u, v being Vector of V
for a being Element of K st u in U & v in U & ( not u = v or a <> - (1_ K) or u = 0. V ) holds
Lin ((U \ {u}) \/ {(u + (a * v))}) = Lin U
let V be VectSp of K; :: thesis: for U being finite Subset of V
for u, v being Vector of V
for a being Element of K st u in U & v in U & ( not u = v or a <> - (1_ K) or u = 0. V ) holds
Lin ((U \ {u}) \/ {(u + (a * v))}) = Lin U
let U be finite Subset of V; :: thesis: for u, v being Vector of V
for a being Element of K st u in U & v in U & ( not u = v or a <> - (1_ K) or u = 0. V ) holds
Lin ((U \ {u}) \/ {(u + (a * v))}) = Lin U
let u, v be Vector of V; :: thesis: for a being Element of K st u in U & v in U & ( not u = v or a <> - (1_ K) or u = 0. V ) holds
Lin ((U \ {u}) \/ {(u + (a * v))}) = Lin U
let a be Element of K; :: thesis: ( u in U & v in U & ( not u = v or a <> - (1_ K) or u = 0. V ) implies Lin ((U \ {u}) \/ {(u + (a * v))}) = Lin U )
assume that
A1: ( u in U & v in U ) and
A2: ( not u = v or a <> - (1_ K) or u = 0. V ) ; :: thesis: Lin ((U \ {u}) \/ {(u + (a * v))}) = Lin U
set UU = U \ {u};
set ua = u + (a * v);
U c= the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))}))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in U or x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) )
assume A3: x in U ; :: thesis: x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))}))

per cases ( x = u or x <> u ) ;

suppose A4: x = u ; :: thesis: x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))}))

per cases ( u <> v or u = v ) ;

suppose u <> v ; :: thesis: x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))}))

then ( v in U \ {u} & u + (a * v) in {(u + (a * v))} ) by A1, TARSKI:def 1, ZFMISC_1:64;
then A5: ( v in (U \ {u}) \/ {(u + (a * v))} & u + (a * v) in (U \ {u}) \/ {(u + (a * v))} ) by XBOOLE_0:def 3;
then A6: ( v in Lin ((U \ {u}) \/ {(u + (a * v))}) & u + (a * v) in Lin ((U \ {u}) \/ {(u + (a * v))}) ) by VECTSP_7:13;
(- a) * v in Lin ((U \ {u}) \/ {(u + (a * v))}) by A5, VECTSP_4:29, VECTSP_7:13;
then A7: (u + (a * v)) + ((- a) * v) in Lin ((U \ {u}) \/ {(u + (a * v))}) by A6, VECTSP_4:28;
(u + (a * v)) + ((- a) * v) = (u + (a * v)) - (a * v) by VECTSP_1:68
.= u + ((a * v) - (a * v)) by RLVECT_1:def 6
.= u + (0. V) by VECTSP_1:63
.= u by RLVECT_1:def 7 ;
hence x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) by A4, A7, STRUCT_0:def 5; :: thesis: verum

end;

suppose A8: u = v ; :: thesis: x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))}))

per cases ( a <> - (1_ K) or u = 0. V ) by A2, A8;

suppose a <> - (1_ K) ; :: thesis: x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))}))

then 0. K <> (- (1_ K)) - a by VECTSP_1:66;
then 0. K <> - ((- (1_ K)) - a) by VECTSP_1:86;
then A9: 0. K <> a + (1_ K) by VECTSP_1:89;
u + (a * v) = ((1_ K) * u) + (a * u) by A8, VECTSP_1:def 26
.= ((1. K) + a) * u by VECTSP_1:def 26 ;
then A10: (((1. K) + a) " ) * (u + (a * v)) = u by A9, VECTSP_1:67;
u + (a * v) in {(u + (a * v))} by TARSKI:def 1;
then u + (a * v) in (U \ {u}) \/ {(u + (a * v))} by XBOOLE_0:def 3;
then u in Lin ((U \ {u}) \/ {(u + (a * v))}) by A10, VECTSP_4:29, VECTSP_7:13;
hence x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) by A4, STRUCT_0:def 5; :: thesis: verum

end;

suppose u = 0. V ; :: thesis: x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))}))

then x in Lin ((U \ {u}) \/ {(u + (a * v))}) by A4, VECTSP_4:25;
hence x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) by STRUCT_0:def 5; :: thesis: verum

end;

end;

end;

end;

end;

suppose x <> u ; :: thesis: x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))}))

then x in U \ {u} by A3, ZFMISC_1:64;
then x in (U \ {u}) \/ {(u + (a * v))} by XBOOLE_0:def 3;
then x in Lin ((U \ {u}) \/ {(u + (a * v))}) by VECTSP_7:13;
hence x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) by STRUCT_0:def 5; :: thesis: verum

end;

end;

end;

then ( Lin ((U \ {u}) \/ {(u + (a * v))}) is Subspace of Lin U & Lin U is Subspace of Lin ((U \ {u}) \/ {(u + (a * v))}) ) by A1, Th13, VECTSP_9:20;
then ( the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) c= the carrier of (Lin U) & the carrier of (Lin U) c= the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) ) by VECTSP_4:def 2;
then the carrier of (Lin U) = the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) by XBOOLE_0:def 10;
hence Lin ((U \ {u}) \/ {(u + (a * v))}) = Lin U by VECTSP_4:37; :: thesis: verum