let K be Field; :: thesis: for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)] holds
(t * w) |-- W,(Lin {y}) = [(t * x),((t * r) * v)]
let V be VectSp of K; :: thesis: for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)] holds
(t * w) |-- W,(Lin {y}) = [(t * x),((t * r) * v)]
let v be Vector of V; :: thesis: for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)] holds
(t * w) |-- W,(Lin {y}) = [(t * x),((t * r) * v)]
let X be Subspace of V; :: thesis: for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)] holds
(t * w) |-- W,(Lin {y}) = [(t * x),((t * r) * v)]
let y be Vector of (X + (Lin {v})); :: thesis: for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)] holds
(t * w) |-- W,(Lin {y}) = [(t * x),((t * r) * v)]
let W be Subspace of X + (Lin {v}); :: thesis: ( v = y & X = W & not v in X implies for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)] holds
(t * w) |-- W,(Lin {y}) = [(t * x),((t * r) * v)] )
assume A1: ( v = y & X = W & not v in X ) ; :: thesis: for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)] holds
(t * w) |-- W,(Lin {y}) = [(t * x),((t * r) * v)]
then A2: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by Th15;
let w be Vector of (X + (Lin {v})); :: thesis: for x being Vector of X
for t, r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)] holds
(t * w) |-- W,(Lin {y}) = [(t * x),((t * r) * v)]
let x be Vector of X; :: thesis: for t, r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)] holds
(t * w) |-- W,(Lin {y}) = [(t * x),((t * r) * v)]
let t, r be Element of K; :: thesis: ( w |-- W,(Lin {y}) = [x,(r * v)] implies (t * w) |-- W,(Lin {y}) = [(t * x),((t * r) * v)] )
assume A3: w |-- W,(Lin {y}) = [x,(r * v)] ; :: thesis: (t * w) |-- W,(Lin {y}) = [(t * x),((t * r) * v)]
reconsider z = x as Vector of (X + (Lin {v})) by A1, VECTSP_4:18;
reconsider u = x as Vector of V by VECTSP_4:18;
A4: t * z = t * u by VECTSP_4:22
.= t * x by VECTSP_4:22 ;
A5: (t * r) * y = (t * r) * v by A1, VECTSP_4:22;
A6: t * z in W by A1, A4, STRUCT_0:def 5;
A7: (t * r) * y in Lin {y} by Th4;
r * y = r * v by A1, VECTSP_4:22;
then t * w = t * (z + (r * y)) by A2, A3, Th7
.= (t * z) + (t * (r * y)) by VECTSP_1:def 26
.= (t * z) + ((t * r) * y) by VECTSP_1:def 26 ;
hence (t * w) |-- W,(Lin {y}) = [(t * x),((t * r) * v)] by A2, A4, A5, A6, A7, Th6; :: thesis: verum