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