let V be Z_Module; LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is modular
set S = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #);
for A, B, C being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) st A [= C holds
A "\/" (B "/\" C) = (A "\/" B) "/\" C
proof
let A,
B,
C be
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #);
( A [= C implies A "\/" (B "/\" C) = (A "\/" B) "/\" C )
reconsider W1 =
A,
W2 =
B,
W3 =
C as
strict Submodule of
V by Def16;
assume A1:
A [= C
;
A "\/" (B "/\" C) = (A "\/" B) "/\" C
reconsider AB =
W1 + W2 as
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #)
by Def16;
reconsider BC =
W2 /\ W3 as
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #)
by Def16;
W1 + W3 =
A "\/" C
by Def21
.=
W3
by A1
;
then A2:
W1 is
Submodule of
W3
by Th98;
thus A "\/" (B "/\" C) =
(SubJoin V) . (
A,
BC)
by Def22
.=
W1 + (W2 /\ W3)
by Def21
.=
(W1 + W2) /\ W3
by A2, Th118
.=
(SubMeet V) . (
AB,
C)
by Def22
.=
(A "\/" B) "/\" C
by Def21
;
verum
end;
hence
LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is modular
; verum