let R be Ring; for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice
let V be RightMod of R; LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice
set S = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #);
A1:
for A, B being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds A "/\" B = B "/\" A
A4:
for A, B being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds (A "/\" B) "\/" B = B
proof
let A,
B be
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #);
(A "/\" B) "\/" B = B
consider W1 being
strict Submodule of
V such that A5:
W1 = A
by Def3;
consider W2 being
strict Submodule of
V such that A6:
W2 = B
by Def3;
reconsider AB =
W1 /\ W2 as
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #)
by Def3;
thus (A "/\" B) "\/" B =
(SubJoin V) . (
(A "/\" B),
B)
by LATTICES:def 1
.=
(SubJoin V) . (
((SubMeet V) . (A,B)),
B)
by LATTICES:def 2
.=
(SubJoin V) . (
AB,
B)
by A5, A6, Def7
.=
(W1 /\ W2) + W2
by A6, Def6
.=
B
by A6, Lm8, RMOD_2:29
;
verum
end;
A7:
for A, B, C being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds A "/\" (B "/\" C) = (A "/\" B) "/\" C
proof
let A,
B,
C be
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #);
A "/\" (B "/\" C) = (A "/\" B) "/\" C
consider W1 being
strict Submodule of
V such that A8:
W1 = A
by Def3;
consider W2 being
strict Submodule of
V such that A9:
W2 = B
by Def3;
consider W3 being
strict Submodule of
V such that A10:
W3 = C
by Def3;
reconsider AB =
W1 /\ W2,
BC =
W2 /\ W3 as
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #)
by Def3;
thus A "/\" (B "/\" C) =
(SubMeet V) . (
A,
(B "/\" C))
by LATTICES:def 2
.=
(SubMeet V) . (
A,
((SubMeet V) . (B,C)))
by LATTICES:def 2
.=
(SubMeet V) . (
A,
BC)
by A9, A10, Def7
.=
W1 /\ (W2 /\ W3)
by A8, Def7
.=
(W1 /\ W2) /\ W3
by Th15
.=
(SubMeet V) . (
AB,
C)
by A10, Def7
.=
(SubMeet V) . (
((SubMeet V) . (A,B)),
C)
by A8, A9, Def7
.=
(SubMeet V) . (
(A "/\" B),
C)
by LATTICES:def 2
.=
(A "/\" B) "/\" C
by LATTICES:def 2
;
verum
end;
A11:
for A, B, C being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds A "\/" (B "\/" C) = (A "\/" B) "\/" C
proof
let A,
B,
C be
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #);
A "\/" (B "\/" C) = (A "\/" B) "\/" C
consider W1 being
strict Submodule of
V such that A12:
W1 = A
by Def3;
consider W2 being
strict Submodule of
V such that A13:
W2 = B
by Def3;
consider W3 being
strict Submodule of
V such that A14:
W3 = C
by Def3;
reconsider AB =
W1 + W2,
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,
((SubJoin V) . (B,C)))
by LATTICES:def 1
.=
(SubJoin V) . (
A,
BC)
by A13, A14, Def6
.=
W1 + (W2 + W3)
by A12, Def6
.=
(W1 + W2) + W3
by Th6
.=
(SubJoin V) . (
AB,
C)
by A14, Def6
.=
(SubJoin V) . (
((SubJoin V) . (A,B)),
C)
by A12, A13, Def6
.=
(SubJoin V) . (
(A "\/" B),
C)
by LATTICES:def 1
.=
(A "\/" B) "\/" C
by LATTICES:def 1
;
verum
end;
A15:
for A, B being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds A "/\" (A "\/" B) = A
proof
let A,
B be
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #);
A "/\" (A "\/" B) = A
consider W1 being
strict Submodule of
V such that A16:
W1 = A
by Def3;
consider W2 being
strict Submodule of
V such that A17:
W2 = B
by Def3;
reconsider AB =
W1 + W2 as
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #)
by Def3;
thus A "/\" (A "\/" B) =
(SubMeet V) . (
A,
(A "\/" B))
by LATTICES:def 2
.=
(SubMeet V) . (
A,
((SubJoin V) . (A,B)))
by LATTICES:def 1
.=
(SubMeet V) . (
A,
AB)
by A16, A17, Def6
.=
W1 /\ (W1 + W2)
by A16, Def7
.=
A
by A16, Lm9, RMOD_2:29
;
verum
end;
for A, B being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds A "\/" B = B "\/" A
then
( LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is join-commutative & LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is join-associative & LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is meet-absorbing & LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is meet-commutative & LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is meet-associative & LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is join-absorbing )
by A11, A4, A1, A7, A15, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
hence
LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice
; verum