let R be Ring; for V being LeftMod 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 LeftMod 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
VECTSP_4:def 1 for b1 being Element of the carrier of R
for b2 being Element of the carrier of V holds
( not b2 in V3 or b1 * b2 in V3 )proof
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 Element of R; for b1 being Element of the carrier of V holds
( not b1 in V3 or a * b1 in V3 )
let v be Vector of V; ( not v in V3 or 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, VECTSP_1:def 14;
( a * v1 in V1 & a * v2 in V2 )
by A1, A11;
hence
a * v in V3
by A2, A12; verum