let x be set ; :: thesis: for V being RealLinearSpace
for v, w1, w2 being VECTOR of V holds
( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) )
let V be RealLinearSpace; :: thesis: for v, w1, w2 being VECTOR of V holds
( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) )
let v, w1, w2 be VECTOR of V; :: thesis: ( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) )
thus ( x in v + (Z_Lin {w1,w2}) implies ex a, b being Integer st x = (v + (a * w1)) + (b * w2) ) :: thesis: ( ex a, b being Integer st x = (v + (a * w1)) + (b * w2) implies x in v + (Z_Lin {w1,w2}) )
proof
assume x in v + (Z_Lin {w1,w2}) ; :: thesis: ex a, b being Integer st x = (v + (a * w1)) + (b * w2)
then consider u being VECTOR of V such that
A1: x = v + u and
A2: u in Z_Lin {w1,w2} ;
consider a, b being Integer such that
A3: u = (a * w1) + (b * w2) by A2, Th19;
take a ; :: thesis: ex b being Integer st x = (v + (a * w1)) + (b * w2)
take b ; :: thesis: x = (v + (a * w1)) + (b * w2)
thus x = (v + (a * w1)) + (b * w2) by A1, A3, RLVECT_1:def 3; :: thesis: verum
end;
given a, b being Integer such that A4: x = (v + (a * w1)) + (b * w2) ; :: thesis: x in v + (Z_Lin {w1,w2})
(a * w1) + (b * w2) in Z_Lin {w1,w2} by Th19;
then v + ((a * w1) + (b * w2)) in v + (Z_Lin {w1,w2}) ;
hence x in v + (Z_Lin {w1,w2}) by A4, RLVECT_1:def 3; :: thesis: verum