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
consider u being VECTOR of V such that
A3: a * v = v + u and
A4: u in W by A2;
u = u + (0. V) by RLVECT_1:10
.= u + (v - v) by RLVECT_1:28
.= (a * v) - v by A3, RLVECT_1:def 6
.= (a * v) - (1 * v) by RLVECT_1:def 9
.= (a - 1) * v by RLVECT_1:49 ;
then ( ((a - 1) " ) * u = (((a - 1) " ) * (a - 1)) * v & a - 1 <> 0 ) by A1, RLVECT_1:def 9;
then 1 * v = ((a - 1) " ) * u by XCMPLX_0:def 7;
then v = ((a - 1) " ) * u by RLVECT_1:def 9;
hence v in W by A4, Th15; :: thesis: verum