let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is Element of V : ( v in V1 & u in V2 ) } holds
V3 is linearly-closed
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is Element 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 v, u is Element 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 v, u is Element of V : ( v in V1 & u in V2 ) }
; V3 is linearly-closed
thus
for v, u being Element of V st v in V3 & u in V3 holds
v + u in V3
VECTSP_4:def 1 for a being Element of GF
for v being Element of V st v in V3 holds
a * v in V3proof
let v,
u be
Element 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 v1,
v2 being
Element of
V such that A5:
v = v1 + v2
and A6:
(
v1 in V1 &
v2 in V2 )
by A2, A3;
consider u1,
u2 being
Element 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 GF; for v being Element of V st v in V3 holds
a * v in V3
let v be Element of V; ( v in V3 implies a * v in V3 )
assume
v in V3
; a * v in V3
then consider v1, v2 being Element 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