let V be RealUnitarySpace; :: thesis: for W being Subspace of V
for v being VECTOR of V
for a being Real st a <> 1 & a * v in v + W holds
v in W
let W be Subspace of V; :: thesis: for v being VECTOR of V
for a being Real st a <> 1 & a * v in v + W holds
v in W
let v be VECTOR of V; :: thesis: for a being Real st a <> 1 & a * v in v + W holds
v in W
let a be Real; :: thesis: ( a <> 1 & a * v in v + W implies v in W )
assume that
A1: a <> 1 and
A2: a * v in v + W ; :: thesis: v in W
A3: a - 1 <> 0 by A1;
consider u being VECTOR of V such that
A4: a * 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
.= (a * v) - v by A4, RLVECT_1:def 3
.= (a * v) - (1 * v) by RLVECT_1:def 8
.= (a - 1) * v by RLVECT_1:35 ;
then ((a - 1) ") * u = (((a - 1) ") * (a - 1)) * v by RLVECT_1:def 7;
then 1 * v = ((a - 1) ") * u by A3, XCMPLX_0:def 7;
then v = ((a - 1) ") * u by RLVECT_1:def 8;
hence v in W by A5, Th15; :: thesis: verum