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) by VECTSP_1:def 17

.= (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 by VECTSP_1:def 17;

hence v in W by A5, Th21; :: thesis: verum

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) by VECTSP_1:def 17

.= (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 by VECTSP_1:def 17;

hence v in W by A5, Th21; :: thesis: verum