let R be Ring; for V being RightMod of R
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 V be RightMod of R; 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
RMOD_2:def 1 for a being Scalar of R
for v being Vector of V st v in V3 holds
v * a 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 Scalar of R; for v being Vector of V st v in V3 holds
v * a in V3
let v be Vector of V; ( v in V3 implies v * a in V3 )
assume
v in V3
; v * a 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:
v * a = (v1 * a) + (v2 * a)
by A10, VECTSP_2:def 9;
( v1 * a in V1 & v2 * a in V2 )
by A1, A11;
hence
v * a in V3
by A2, A12; verum