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 and
A2: v in U and
A3: ( not u = v or a <> - (1_ K) or u = 0. V ) ; :: thesis: Lin ((U \ {u}) \/ {(u + (a * v))}) = Lin U
set ua = u + (a * v);
set UU = U \ {u};
U c= the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))}))

proof

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

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

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

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

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

A7: (u + (a * v)) + ((- a) * v) = (u + (a * v)) - (a * v) by VECTSP_1:21
.= u + ((a * v) - (a * v)) by RLVECT_1:def 3
.= u + (0. V) by VECTSP_1:16
.= u by RLVECT_1:def 4 ;
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 A8: u + (a * v) in Lin ((U \ {u}) \/ {(u + (a * v))}) by VECTSP_7:8;
v in U \ {u} by A2, A6, ZFMISC_1:56;
then v in (U \ {u}) \/ {(u + (a * v))} by XBOOLE_0:def 3;
then (- a) * v in Lin ((U \ {u}) \/ {(u + (a * v))}) by VECTSP_4:21, VECTSP_7:8;
then (u + (a * v)) + ((- a) * v) in Lin ((U \ {u}) \/ {(u + (a * v))}) by A8, VECTSP_4:20;
hence x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) by A5, A7, STRUCT_0:def 5; :: thesis: verum

end;

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

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

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:19;
then 0. K <> - ((- (1_ K)) - a) by VECTSP_1:28;
then A10: 0. K <> a + (1_ K) by VECTSP_1:31;
u + (a * v) in {(u + (a * v))} by TARSKI:def 1;
then A11: u + (a * v) in (U \ {u}) \/ {(u + (a * v))} by XBOOLE_0:def 3;
u + (a * v) = ((1_ K) * u) + (a * u) by A9
.= ((1. K) + a) * u by VECTSP_1:def 15 ;
then (((1. K) + a) ") * (u + (a * v)) = u by A10, VECTSP_1:20;
then u in Lin ((U \ {u}) \/ {(u + (a * v))}) by A11, VECTSP_4:21, VECTSP_7:8;
hence x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) by A5, 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 A5, VECTSP_4:17;
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 A4, ZFMISC_1:56;
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:8;
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 is Subspace of Lin ((U \ {u}) \/ {(u + (a * v))}) by VECTSP_9:16;
then A12: the carrier of (Lin U) c= the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) by VECTSP_4:def 2;
Lin ((U \ {u}) \/ {(u + (a * v))}) is Subspace of Lin U by A1, A2, Th13;
then the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) c= the carrier of (Lin U) by VECTSP_4:def 2;
then the carrier of (Lin U) = the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) by A12;
hence Lin ((U \ {u}) \/ {(u + (a * v))}) = Lin U by VECTSP_4:29; :: thesis: verum