let V be RealLinearSpace; :: 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 Real 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 Real 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 Real 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 Real 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 Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)] )
assume that
A1: v = y and
A2: X = W and
A3: not v in X ; :: thesis: for w being VECTOR of (X + (Lin {v}))
for x being VECTOR of X
for t, r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
A4: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th11;
let w be VECTOR of (X + (Lin {v})); :: thesis: for x being VECTOR of X
for t, r being Real 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 Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let t, r be Real; :: thesis: ( w |-- (W,(Lin {y})) = [x,(r * v)] implies (t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)] )
assume A5: 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 A2, RLSUB_1:10;
r * y = r * v by A1, RLSUB_1:14;
then A6: t * w = t * (z + (r * y)) by A4, A5, Th3
.= (t * z) + (t * (r * y)) by RLVECT_1:def 5
.= (t * z) + ((t * r) * y) by RLVECT_1:def 7 ;
reconsider u = x as VECTOR of V by RLSUB_1:10;
A7: (t * r) * y in Lin {y} by RLVECT_4:8;
A8: (t * r) * y = (t * r) * v by A1, RLSUB_1:14;
A9: t * z = t * u by RLSUB_1:14
.= t * x by RLSUB_1:14 ;
then t * z in W by A2;
hence (t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)] by A4, A9, A8, A7, A6, Th2; :: thesis: verum