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})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. 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})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. 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})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. 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})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. 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})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. 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})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)] )
assume that
A1:
v = y
and
A2:
X = W
and
A3:
not v in X
; for w being Vector of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. 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})); ( w in X implies w |-- (W,(Lin {y})) = [w,(0. V)] )
assume
w in X
; w |-- (W,(Lin {y})) = [w,(0. V)]
then
w |-- (W,(Lin {y})) = [w,(0. (X + (Lin {v})))]
by A2, A4, Th9;
hence
w |-- (W,(Lin {y})) = [w,(0. V)]
by VECTSP_4:11; verum