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 w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- W,(Lin {y}) = [x1,(r1 * v)] & w2 |-- W,(Lin {y}) = [x2,(r2 * v)] holds
(w1 + w2) |-- W,(Lin {y}) = [(x1 + x2),((r1 + r2) * 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 w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- W,(Lin {y}) = [x1,(r1 * v)] & w2 |-- W,(Lin {y}) = [x2,(r2 * v)] holds
(w1 + w2) |-- W,(Lin {y}) = [(x1 + x2),((r1 + r2) * 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 w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- W,(Lin {y}) = [x1,(r1 * v)] & w2 |-- W,(Lin {y}) = [x2,(r2 * v)] holds
(w1 + w2) |-- W,(Lin {y}) = [(x1 + x2),((r1 + r2) * 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 w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- W,(Lin {y}) = [x1,(r1 * v)] & w2 |-- W,(Lin {y}) = [x2,(r2 * v)] holds
(w1 + w2) |-- W,(Lin {y}) = [(x1 + x2),((r1 + r2) * v)]
let W be Subspace of X + (Lin {v}); :: thesis: ( v = y & X = W & not v in X implies for w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- W,(Lin {y}) = [x1,(r1 * v)] & w2 |-- W,(Lin {y}) = [x2,(r2 * v)] holds
(w1 + w2) |-- W,(Lin {y}) = [(x1 + x2),((r1 + r2) * v)] )
assume A1: ( v = y & X = W & not v in X ) ; :: thesis: for w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- W,(Lin {y}) = [x1,(r1 * v)] & w2 |-- W,(Lin {y}) = [x2,(r2 * v)] holds
(w1 + w2) |-- W,(Lin {y}) = [(x1 + x2),((r1 + r2) * v)]
then A2: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by Th24;
let w1, w2 be VECTOR of (X + (Lin {v})); :: thesis: for x1, x2 being VECTOR of X
for r1, r2 being Real st w1 |-- W,(Lin {y}) = [x1,(r1 * v)] & w2 |-- W,(Lin {y}) = [x2,(r2 * v)] holds
(w1 + w2) |-- W,(Lin {y}) = [(x1 + x2),((r1 + r2) * v)]
let x1, x2 be VECTOR of X; :: thesis: for r1, r2 being Real st w1 |-- W,(Lin {y}) = [x1,(r1 * v)] & w2 |-- W,(Lin {y}) = [x2,(r2 * v)] holds
(w1 + w2) |-- W,(Lin {y}) = [(x1 + x2),((r1 + r2) * v)]
let r1, r2 be Real; :: thesis: ( w1 |-- W,(Lin {y}) = [x1,(r1 * v)] & w2 |-- W,(Lin {y}) = [x2,(r2 * v)] implies (w1 + w2) |-- W,(Lin {y}) = [(x1 + x2),((r1 + r2) * v)] )
assume A3: ( w1 |-- W,(Lin {y}) = [x1,(r1 * v)] & w2 |-- W,(Lin {y}) = [x2,(r2 * v)] ) ; :: thesis: (w1 + w2) |-- W,(Lin {y}) = [(x1 + x2),((r1 + r2) * v)]
reconsider z1 = x1, z2 = x2 as VECTOR of V by RLSUB_1:18;
reconsider y1 = x1, y2 = x2 as VECTOR of (X + (Lin {v})) by A1, RLSUB_1:18;
A4: ( r1 * v = r1 * y & r2 * v = r2 * y ) by A1, RLSUB_1:22;
then ( y1 in W & y2 in W ) by A2, A3, Th17;
then A5: y1 + y2 in W by RLSUB_1:28;
(r1 + r2) * v = (r1 + r2) * y by A1, RLSUB_1:22;
then A6: (r1 + r2) * v in Lin {y} by RLVECT_4:11;
( w1 = y1 + (r1 * y) & w2 = y2 + (r2 * y) ) by A2, A3, A4, Th16;
then A7: w1 + w2 = ((y1 + (r1 * y)) + y2) + (r2 * y) by RLVECT_1:def 6
.= ((y1 + y2) + (r1 * y)) + (r2 * y) by RLVECT_1:def 6
.= (y1 + y2) + ((r1 * y) + (r2 * y)) by RLVECT_1:def 6
.= (y1 + y2) + ((r1 + r2) * y) by RLVECT_1:def 9 ;
A8: (r1 + r2) * y = (r1 + r2) * v by A1, RLSUB_1:22;
y1 + y2 = z1 + z2 by RLSUB_1:21
.= x1 + x2 by RLSUB_1:21 ;
hence (w1 + w2) |-- W,(Lin {y}) = [(x1 + x2),((r1 + r2) * v)] by A2, A5, A6, A7, A8, Th15; :: thesis: verum