let R be Ring; for V being RightMod of holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice
let V be RightMod of ; LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice
set S = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #);
ex C being Element of st
for A being Element of 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
by Def3;
take
C
;
for A being Element of holds
( C "\/" A = C & A "\/" C = C )
let A be
Element of ;
( 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
.=
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
;
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
;
verum
end;
hence
LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice
by Th63, LATTICES:def 14; verum