let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V
for z being Complex
for W being Subspace of V st z <> 1r & z * v in v + W holds
v in W
let v be VECTOR of V; :: thesis: for z being Complex
for W being Subspace of V st z <> 1r & z * v in v + W holds
v in W
let z be Complex; :: thesis: for W being Subspace of V st z <> 1r & z * v in v + W holds
v in W
let W be Subspace of V; :: thesis: ( z <> 1r & z * v in v + W implies v in W )
assume that
A1: z <> 1r and
A2: z * v in v + W ; :: thesis: v in W
A3: z - 1r <> 0 by A1;
consider u being VECTOR of V such that
A4: z * v = v + u and
A5: u in W by A2;
u = u + (0. V) by RLVECT_1:4
.= u + (v - v) by RLVECT_1:15
.= (z * v) - v by A4, RLVECT_1:def 3
.= (z * v) - (1r * v) by Def5
.= (z - 1r) * v by Th11 ;
then ((z - 1r) ") * u = (((z - 1r) ") * (z - 1r)) * v by Def4;
then 1r * v = ((z - 1r) ") * u by A3, XCMPLX_0:def 7;
then v = ((z - 1r) ") * u by Def5;
hence v in W by A5, Th41; :: thesis: verum