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))}))

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

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

then
Lin U is Subspace of Lin ((U \ {u}) \/ {(u + (a * v))})
by VECTSP_9:16;
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))}))

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

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

end;

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

end;

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

end;

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;.= 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

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

end;

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

end;

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, VECTSP_1:def 17

.= ((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;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, VECTSP_1:def 17

.= ((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

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;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

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