let K be Field; 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; 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; 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; 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})); 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}); ( 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 that
A1:
v = y
and
A2:
X = W
and
A3:
not v in X
; 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)]
A4:
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
by A1, A2, A3, Th14;
let w be 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 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 t, r be Element of K; ( 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)]
; (t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
reconsider z = x as Vector of (X + (Lin {v})) by A2, VECTSP_4:10;
r * y = r * v
by A1, VECTSP_4:14;
then A6: t * w =
t * (z + (r * y))
by A4, A5, Th6
.=
(t * z) + (t * (r * y))
by VECTSP_1:def 14
.=
(t * z) + ((t * r) * y)
by VECTSP_1:def 16
;
reconsider u = x as Vector of V by VECTSP_4:10;
A7:
(t * r) * y in Lin {y}
by Th3;
A8:
(t * r) * y = (t * r) * v
by A1, VECTSP_4:14;
A9: t * z =
t * u
by VECTSP_4:14
.=
t * x
by VECTSP_4: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, Th5; verum