let V be RealLinearSpace; for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where u, v is VECTOR of V : ( v in V1 & u in V2 ) } holds
V3 is linearly-closed
let V1, V2, V3 be Subset of V; ( V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where u, v is VECTOR of V : ( v in V1 & u in V2 ) } implies V3 is linearly-closed )
assume that
A1:
( V1 is linearly-closed & V2 is linearly-closed )
and
A2:
V3 = { (v + u) where u, v is VECTOR of V : ( v in V1 & u in V2 ) }
; V3 is linearly-closed
thus
for v, u being VECTOR of V st v in V3 & u in V3 holds
v + u in V3
RLSUB_1:def 1 for a being Real
for v being VECTOR of V st v in V3 holds
a * v in V3proof
let v,
u be
VECTOR of
V;
( v in V3 & u in V3 implies v + u in V3 )
assume that A3:
v in V3
and A4:
u in V3
;
v + u in V3
consider v2,
v1 being
VECTOR of
V such that A5:
v = v1 + v2
and A6:
(
v1 in V1 &
v2 in V2 )
by A2, A3;
consider u2,
u1 being
VECTOR of
V such that A7:
u = u1 + u2
and A8:
(
u1 in V1 &
u2 in V2 )
by A2, A4;
A9:
v + u =
((v1 + v2) + u1) + u2
by A5, A7, RLVECT_1:def 3
.=
((v1 + u1) + v2) + u2
by RLVECT_1:def 3
.=
(v1 + u1) + (v2 + u2)
by RLVECT_1:def 3
;
(
v1 + u1 in V1 &
v2 + u2 in V2 )
by A1, A6, A8;
hence
v + u in V3
by A2, A9;
verum
end;
let a be Real; for v being VECTOR of V st v in V3 holds
a * v in V3
let v be VECTOR of V; ( v in V3 implies a * v in V3 )
assume
v in V3
; a * v in V3
then consider v2, v1 being VECTOR of V such that
A10:
v = v1 + v2
and
A11:
( v1 in V1 & v2 in V2 )
by A2;
A12:
a * v = (a * v1) + (a * v2)
by A10, RLVECT_1:def 5;
( a * v1 in V1 & a * v2 in V2 )
by A1, A11;
hence
a * v in V3
by A2, A12; verum