let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 1_Lattice
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 1_Lattice
set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);
ex C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) st
for A being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds
( C "\/" A = C & A "\/" C = C )
proof
consider W9 being
strict Subspace of
M such that A1:
the
carrier of
W9 = the
carrier of
((Omega). M)
;
reconsider C =
W9 as
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #)
by Def3;
take
C
;
for A being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds
( C "\/" A = C & A "\/" C = C )
let A be
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #);
( C "\/" A = C & A "\/" C = C )
consider W being
strict Subspace of
M such that A2:
W = A
by Def3;
A3:
C is
Subspace of
(Omega). M
by Lm6;
thus C "\/" A =
(SubJoin M) . (
C,
A)
by LATTICES:def 1
.=
W9 + W
by A2, Def7
.=
((Omega). M) + W
by A1, Lm5
.=
ModuleStr(# the
carrier of
M, the
addF of
M, the
ZeroF of
M, the
lmult of
M #)
by Th11
.=
C
by A1, A3, VECTSP_4:31
;
A "\/" C = C
thus A "\/" C =
(SubJoin M) . (
A,
C)
by LATTICES:def 1
.=
W + W9
by A2, Def7
.=
W + ((Omega). M)
by A1, Lm5
.=
ModuleStr(# the
carrier of
M, the
addF of
M, the
ZeroF of
M, the
lmult of
M #)
by Th11
.=
C
by A1, A3, VECTSP_4:31
;
verum
end;
hence
LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 1_Lattice
by Th57, LATTICES:def 14; verum