let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V
for z being Complex
for W being Subspace of V st z <> 0 & (z * v) + W = the carrier of W holds
v in W
let v be VECTOR of V; :: thesis: for z being Complex
for W being Subspace of V st z <> 0 & (z * v) + W = the carrier of W holds
v in W
let z be Complex; :: thesis: for W being Subspace of V st z <> 0 & (z * v) + W = the carrier of W holds
v in W
let W be Subspace of V; :: thesis: ( z <> 0 & (z * v) + W = the carrier of W implies v in W )
assume that
A1: z <> 0 and
A2: (z * v) + W = the carrier of W ; :: thesis: v in W
assume not v in W ; :: thesis: contradiction
then not 1r * v in W by Def2;
then not ((z " ) * z) * v in W by A1, XCMPLX_0:def 7;
then not (z " ) * (z * v) in W by Def2;
then A3: not z * v in W by Th41;
( 0. V in W & (z * v) + (0. V) = z * v ) by Th37, RLVECT_1:10;
then z * v in { ((z * v) + u) where u is VECTOR of V : u in W } ;
hence contradiction by A2, A3, STRUCT_0:def 5; :: thesis: verum