let R be Ring; for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice
let V be RightMod of R; LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice
set S = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #);
ex C being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) st
for A being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds
( C "\/" A = C & A "\/" C = C )
proof
consider W9 being
strict Submodule of
V such that A1:
the
carrier of
W9 = the
carrier of
((Omega). V)
;
reconsider C =
W9 as
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #)
by Def3;
take
C
;
for A being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds
( C "\/" A = C & A "\/" C = C )
let A be
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #);
( C "\/" A = C & A "\/" C = C )
consider W being
strict Submodule of
V such that A2:
W = A
by Def3;
A3:
C is
Submodule of
(Omega). V
by Lm5;
thus C "\/" A =
(SubJoin V) . (
C,
A)
by LATTICES:def 1
.=
W9 + W
by A2, Def6
.=
((Omega). V) + W
by A1, Lm4
.=
RightModStr(# the
carrier of
V, the
U7 of
V, the
ZeroF of
V, the
rmult of
V #)
by Th11
.=
C
by A1, A3, RMOD_2:31
;
A "\/" C = C
thus A "\/" C =
(SubJoin V) . (
A,
C)
by LATTICES:def 1
.=
W + W9
by A2, Def6
.=
W + ((Omega). V)
by A1, Lm4
.=
RightModStr(# the
carrier of
V, the
U7 of
V, the
ZeroF of
V, the
rmult of
V #)
by Th11
.=
C
by A1, A3, RMOD_2:31
;
verum
end;
hence
LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice
by Th47, LATTICES:def 14; verum