let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V
for z being Complex
for W being Subspace of V st v in W holds
(z * v) + W = the carrier of W
let v be VECTOR of V; :: thesis: for z being Complex
for W being Subspace of V st v in W holds
(z * v) + W = the carrier of W
let z be Complex; :: thesis: for W being Subspace of V st v in W holds
(z * v) + W = the carrier of W
let W be Subspace of V; :: thesis: ( v in W implies (z * v) + W = the carrier of W )
assume A1: v in W ; :: thesis: (z * v) + W = the carrier of W
thus (z * v) + W c= the carrier of W :: according to XBOOLE_0:def 10 :: thesis: the carrier of W c= (z * v) + W
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (z * v) + W or x in the carrier of W )
assume x in (z * v) + W ; :: thesis: x in the carrier of W
then consider u being VECTOR of V such that
A2: x = (z * v) + u and
A3: u in W ;
z * v in W by A1, Th40;
then (z * v) + u in W by A3, Th39;
hence x in the carrier of W by A2; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of W or x in (z * v) + W )
assume A4: x in the carrier of W ; :: thesis: x in (z * v) + W
then A5: x in W ;
the carrier of W c= the carrier of V by Def8;
then reconsider y = x as Element of V by A4;
A6: (z * v) + (y - (z * v)) = (y + (z * v)) - (z * v) by RLVECT_1:def 3
.= y + ((z * v) - (z * v)) by RLVECT_1:def 3
.= y + (0. V) by RLVECT_1:15
.= x by RLVECT_1:4 ;
z * v in W by A1, Th40;
then y - (z * v) in W by A5, Th42;
hence x in (z * v) + W by A6; :: thesis: verum