let R be Ring; for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is M_Lattice
let V be RightMod of R; LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is M_Lattice
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 )
assume A1:
A [= C
;
A "\/" (B "/\" C) = (A "\/" B) "/\" C
consider W1 being
strict Submodule of
V such that A2:
W1 = A
by Def3;
consider W3 being
strict Submodule of
V such that A3:
W3 = C
by Def3;
W1 + W3 =
(SubJoin V) . (
A,
C)
by A2, A3, Def6
.=
A "\/" C
by LATTICES:def 1
.=
W3
by A1, A3, LATTICES:def 3
;
then A4:
W1 is
Submodule of
W3
by Th8;
consider W2 being
strict Submodule of
V such that A5:
W2 = B
by Def3;
reconsider AB =
W1 + W2 as
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #)
by Def3;
reconsider BC =
W2 /\ W3 as
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #)
by Def3;
thus A "\/" (B "/\" C) =
(SubJoin V) . (
A,
(B "/\" C))
by LATTICES:def 1
.=
(SubJoin V) . (
A,
((SubMeet V) . (B,C)))
by LATTICES:def 2
.=
(SubJoin V) . (
A,
BC)
by A5, A3, Def7
.=
W1 + (W2 /\ W3)
by A2, Def6
.=
(W1 + W2) /\ W3
by A4, Th31
.=
(SubMeet V) . (
AB,
C)
by A3, Def7
.=
(SubMeet V) . (
((SubJoin V) . (A,B)),
C)
by A2, A5, Def6
.=
(SubMeet V) . (
(A "\/" B),
C)
by LATTICES:def 1
.=
(A "\/" B) "/\" C
by LATTICES:def 2
;
verum
end;
hence
LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is M_Lattice
by Th47, LATTICES:def 12; verum