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 M_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 M_Lattice
set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);
for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) st A [= C holds
A "\/" (B "/\" C) = (A "\/" B) "/\" C
proof
let A,
B,
C be
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #);
( A [= C implies A "\/" (B "/\" C) = (A "\/" B) "/\" C )
assume A1:
A [= C
;
A "\/" (B "/\" C) = (A "\/" B) "/\" C
consider W1 being
strict Subspace of
M such that A2:
W1 = A
by Def3;
consider W3 being
strict Subspace of
M such that A3:
W3 = C
by Def3;
W1 + W3 =
(SubJoin M) . (
A,
C)
by A2, A3, Def7
.=
A "\/" C
by LATTICES:def 1
.=
W3
by A1, A3, LATTICES:def 3
;
then A4:
W1 is
Subspace of
W3
by Th8;
consider W2 being
strict Subspace of
M such that A5:
W2 = B
by Def3;
reconsider AB =
W1 + W2 as
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #)
by Def3;
reconsider BC =
W2 /\ W3 as
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #)
by Def3;
thus A "\/" (B "/\" C) =
(SubJoin M) . (
A,
(B "/\" C))
by LATTICES:def 1
.=
(SubJoin M) . (
A,
((SubMeet M) . (B,C)))
by LATTICES:def 2
.=
(SubJoin M) . (
A,
BC)
by A5, A3, Def8
.=
W1 + (W2 /\ W3)
by A2, Def7
.=
(W1 + W2) /\ W3
by A4, Th30
.=
(SubMeet M) . (
AB,
C)
by A3, Def8
.=
(SubMeet M) . (
((SubJoin M) . (A,B)),
C)
by A2, A5, Def7
.=
(SubMeet M) . (
(A "\/" B),
C)
by LATTICES:def 1
.=
(A "\/" B) "/\" C
by LATTICES:def 2
;
verum
end;
hence
LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice
by Th57, LATTICES:def 12; verum