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 <> 0. GF & (a * v) + W = the carrier of 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 <> 0. GF & (a * v) + W = the carrier of 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 <> 0. GF & (a * v) + W = the carrier of W holds
v in W
let v be Element of V; :: thesis: for W being Subspace of V st a <> 0. GF & (a * v) + W = the carrier of W holds
v in W
let W be Subspace of V; :: thesis: ( a <> 0. GF & (a * v) + W = the carrier of W implies v in W )
assume that
A1: a <> 0. GF and
A2: (a * v) + W = the carrier of W ; :: thesis: v in W
assume not v in W ; :: thesis: contradiction
then not (1_ GF) * v in W ;
then not ((a ") * a) * v in W by A1, VECTSP_1:def 10;
then not (a ") * (a * v) in W by VECTSP_1:def 16;
then A3: not a * v in W by Th21;
( 0. V in W & (a * v) + (0. V) = a * v ) by Th17, RLVECT_1:4;
then a * v in { ((a * v) + u) where u is Vector of V : u in W } ;
hence contradiction by A2, A3; :: thesis: verum