let R be Ring; :: thesis: 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; :: thesis: 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; :: thesis: ( 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
; :: thesis: 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))
:: according to XBOOLE_0:def 10 :: thesis: the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( 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))
;
:: thesis: 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 u, v is Vector of V : ( u in W1 & v in W3 ) }
by Def1;
then consider u1,
v1 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:16;
then A7:
u1 in W1 /\ W2
by A4, Th7;
x in the
carrier of
W2
by A2, XBOOLE_0:def 4;
then
u1 + v1 in W2
by A3, STRUCT_0:def 5;
then
(v1 + u1) - u1 in W2
by A6, RMOD_2:31;
then
v1 + (u1 - u1) in W2
by RLVECT_1:def 6;
then
v1 + (0. V) in W2
by VECTSP_1:66;
then
v1 in W2
by RLVECT_1:def 7;
then
v1 in W2 /\ W3
by A5, Th7;
then
x in (W1 /\ W2) + (W2 /\ W3)
by A3, A7, Th5;
hence
x in the
carrier of
((W1 /\ W2) + (W2 /\ W3))
by STRUCT_0:def 5;
:: thesis: verum
end;
thus
the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
by Lm10; :: thesis: verum