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 w1, w2 being Vector of (X + (Lin {v}))
for x1, x2 being Vector of X
for r1, r2 being Element of K 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 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 w1, w2 being Vector of (X + (Lin {v}))
for x1, x2 being Vector of X
for r1, r2 being Element of K 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 Element of K 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 Element of K 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 Element of K 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 Element of K 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 that
A1: v = y and
A2: X = W and
A3: 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 Element of K 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)]
A4: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th14;
let w1, w2 be Vector of (X + (Lin {v})); :: thesis: for x1, x2 being Vector of X
for r1, r2 being Element of K 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 Element of K 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 Element of K; :: 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 that
A5: w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] and
A6: w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] ; :: thesis: (w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
reconsider y1 = x1, y2 = x2 as Vector of (X + (Lin {v})) by A2, VECTSP_4:10;
A7: r2 * v = r2 * y by A1, VECTSP_4:14;
then A8: y2 in W by A4, A6, Th7;
(r1 + r2) * v = (r1 + r2) * y by A1, VECTSP_4:14;
then A9: (r1 + r2) * v in Lin {y} by Th3;
reconsider z1 = x1, z2 = x2 as Vector of V by VECTSP_4:10;
A10: y1 + y2 = z1 + z2 by VECTSP_4:13
.= x1 + x2 by VECTSP_4:13 ;
A11: r1 * v = r1 * y by A1, VECTSP_4:14;
then y1 in W by A4, A5, Th7;
then A12: y1 + y2 in W by A8, VECTSP_4:20;
A13: w2 = y2 + (r2 * y) by A4, A6, A7, Th6;
w1 = y1 + (r1 * y) by A4, A5, A11, Th6;
then A14: w1 + w2 = ((y1 + (r1 * y)) + y2) + (r2 * y) by A13, RLVECT_1:def 3
.= ((y1 + y2) + (r1 * y)) + (r2 * y) by RLVECT_1:def 3
.= (y1 + y2) + ((r1 * y) + (r2 * y)) by RLVECT_1:def 3
.= (y1 + y2) + ((r1 + r2) * y) by VECTSP_1:def 15 ;
(r1 + r2) * y = (r1 + r2) * v by A1, VECTSP_4:14;
hence (w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)] by A4, A12, A9, A14, A10, Th5; :: thesis: verum