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 ;
then v in (U \ {u}) \/ {(u + (a * v))} by XBOOLE_0:def 3;
then (- a) * v in Lin ((U \ {u}) \/ {(u + (a * v))}) by ;
then (u + (a * v)) + ((- a) * v) in Lin ((U \ {u}) \/ {(u + (a * v))}) by ;
hence x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) by ; :: 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
.= ((1. K) + a) * u by VECTSP_1:def 15 ;
then (((1. K) + a) ") * (u + (a * v)) = u by ;
then u in Lin ((U \ {u}) \/ {(u + (a * v))}) by ;
hence x in the carrier of (Lin ((U \ {u}) \/ {(u + (a * v))})) by ; :: 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 ;
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 ;
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