let R be Ring; for V being RightMod of R
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
let V be RightMod of R; for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
let W1, W2, W3 be Submodule of V; ( W1 is Submodule of W2 implies the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3)) )
assume A1:
W1 is Submodule of W2
; the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
thus
the carrier of (W2 /\ (W1 + W3)) c= the carrier of ((W1 /\ W2) + (W2 /\ W3))
XBOOLE_0:def 10 the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))proof
let x be
object ;
TARSKI:def 3 ( not x in the carrier of (W2 /\ (W1 + W3)) or x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) )
assume
x in the
carrier of
(W2 /\ (W1 + W3))
;
x in the carrier of ((W1 /\ W2) + (W2 /\ W3))
then A2:
x in the
carrier of
W2 /\ the
carrier of
(W1 + W3)
by Def2;
then
x in the
carrier of
(W1 + W3)
by XBOOLE_0:def 4;
then
x in { (u + v) where v, u is Vector of V : ( u in W1 & v in W3 ) }
by Def1;
then consider v1,
u1 being
Vector of
V such that A3:
x = u1 + v1
and A4:
u1 in W1
and A5:
v1 in W3
;
A6:
u1 in W2
by A1, A4, RMOD_2:8;
x in the
carrier of
W2
by A2, XBOOLE_0:def 4;
then
u1 + v1 in W2
by A3;
then
(v1 + u1) - u1 in W2
by A6, RMOD_2:23;
then
v1 + (u1 - u1) in W2
by RLVECT_1:def 3;
then
v1 + (0. V) in W2
by VECTSP_1:19;
then
v1 in W2
by RLVECT_1:def 4;
then A7:
v1 in W2 /\ W3
by A5, Th3;
u1 in W1 /\ W2
by A4, A6, Th3;
then
x in (W1 /\ W2) + (W2 /\ W3)
by A3, A7, Th1;
hence
x in the
carrier of
((W1 /\ W2) + (W2 /\ W3))
;
verum
end;
thus
the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
by Lm10; verum