let R be Ring; :: thesis: for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice
let V be RightMod of R; :: thesis: 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 W' being
strict Submodule of
V such that A1:
the
carrier of
W' = the
carrier of
((Omega). V)
;
reconsider C =
W' as
Element of
LattStr(#
(Submodules V),
(SubJoin V),
(SubMeet V) #)
by Def3;
take
C
;
:: thesis: 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) #);
:: thesis: ( 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 &
RightModStr(# the
carrier of
V,the
U7 of
V,the
U2 of
V,the
rmult of
V #)
= (Omega). V )
by Lm5;
thus C "\/" A =
(SubJoin V) . C,
A
by LATTICES:def 1
.=
W' + W
by A2, Def6
.=
((Omega). V) + W
by A1, Lm4
.=
RightModStr(# the
carrier of
V,the
U7 of
V,the
U2 of
V,the
rmult of
V #)
by Th15
.=
C
by A1, A3, RMOD_2:39
;
:: thesis: A "\/" C = C
thus A "\/" C =
(SubJoin V) . A,
C
by LATTICES:def 1
.=
W + W'
by A2, Def6
.=
W + ((Omega). V)
by A1, Lm4
.=
RightModStr(# the
carrier of
V,the
U7 of
V,the
U2 of
V,the
rmult of
V #)
by Th15
.=
C
by A1, A3, RMOD_2:39
;
:: thesis: verum
end;
hence
LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice
by Th63, LATTICES:def 14; :: thesis: verum