let GF be Field; :: thesis: for V being VectSp of GF
for a being Element of GF
for v being Element of V
for W being Subspace of V st a <> 1_ GF & a * v in v + W holds
v in W
let V be VectSp of GF; :: thesis: for a being Element of GF
for v being Element of V
for W being Subspace of V st a <> 1_ GF & a * v in v + W holds
v in W
let a be Element of GF; :: thesis: for v being Element of V
for W being Subspace of V st a <> 1_ GF & a * v in v + W holds
v in W
let v be Element of V; :: thesis: for W being Subspace of V st a <> 1_ GF & a * v in v + W holds
v in W
let W be Subspace of V; :: thesis: ( a <> 1_ GF & a * v in v + W implies v in W )
assume that
A1: a <> 1_ GF and
A2: a * v in v + W ; :: thesis: v in W
A3: a - (1_ GF) <> 0. GF by A1, RLVECT_1:21;
consider u being Element 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 VECTSP_1:19
.= (a * v) - v by A4, RLVECT_1:def 3
.= (a * v) - ((1_ GF) * v)
.= (a - (1_ GF)) * v by Lm1 ;
then ((a - (1_ GF)) ") * u = (((a - (1_ GF)) ") * (a - (1_ GF))) * v by VECTSP_1:def 16;
then (1_ GF) * v = ((a - (1_ GF)) ") * u by A3, VECTSP_1:def 10;
then v = ((a - (1_ GF)) ") * u ;
hence v in W by A5, Th21; :: thesis: verum