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 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 Lattice
set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);
A1:
for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" B = B "/\" A
A4:
for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds (A "/\" B) "\/" B = B
proof
let A,
B be
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #);
(A "/\" B) "\/" B = B
consider W1 being
strict Subspace of
M such that A5:
W1 = A
by Def3;
consider W2 being
strict Subspace of
M such that A6:
W2 = B
by Def3;
reconsider AB =
W1 /\ W2 as
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #)
by Def3;
thus (A "/\" B) "\/" B =
(SubJoin M) . (
(A "/\" B),
B)
by LATTICES:def 1
.=
(SubJoin M) . (
((SubMeet M) . (A,B)),
B)
by LATTICES:def 2
.=
(SubJoin M) . (
AB,
B)
by A5, A6, Def8
.=
(W1 /\ W2) + W2
by A6, Def7
.=
B
by A6, Lm10, VECTSP_4:29
;
verum
end;
A7:
for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" (B "/\" C) = (A "/\" B) "/\" C
proof
let A,
B,
C be
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #);
A "/\" (B "/\" C) = (A "/\" B) "/\" C
consider W1 being
strict Subspace of
M such that A8:
W1 = A
by Def3;
consider W2 being
strict Subspace of
M such that A9:
W2 = B
by Def3;
consider W3 being
strict Subspace of
M such that A10:
W3 = C
by Def3;
reconsider AB =
W1 /\ W2,
BC =
W2 /\ W3 as
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #)
by Def3;
thus A "/\" (B "/\" C) =
(SubMeet M) . (
A,
(B "/\" C))
by LATTICES:def 2
.=
(SubMeet M) . (
A,
((SubMeet M) . (B,C)))
by LATTICES:def 2
.=
(SubMeet M) . (
A,
BC)
by A9, A10, Def8
.=
W1 /\ (W2 /\ W3)
by A8, Def8
.=
(W1 /\ W2) /\ W3
by Th14
.=
(SubMeet M) . (
AB,
C)
by A10, Def8
.=
(SubMeet M) . (
((SubMeet M) . (A,B)),
C)
by A8, A9, Def8
.=
(SubMeet M) . (
(A "/\" B),
C)
by LATTICES:def 2
.=
(A "/\" B) "/\" C
by LATTICES:def 2
;
verum
end;
A11:
for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "\/" (B "\/" C) = (A "\/" B) "\/" C
proof
let A,
B,
C be
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #);
A "\/" (B "\/" C) = (A "\/" B) "\/" C
consider W1 being
strict Subspace of
M such that A12:
W1 = A
by Def3;
consider W2 being
strict Subspace of
M such that A13:
W2 = B
by Def3;
consider W3 being
strict Subspace of
M such that A14:
W3 = C
by Def3;
reconsider AB =
W1 + W2,
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,
((SubJoin M) . (B,C)))
by LATTICES:def 1
.=
(SubJoin M) . (
A,
BC)
by A13, A14, Def7
.=
W1 + (W2 + W3)
by A12, Def7
.=
(W1 + W2) + W3
by Th6
.=
(SubJoin M) . (
AB,
C)
by A14, Def7
.=
(SubJoin M) . (
((SubJoin M) . (A,B)),
C)
by A12, A13, Def7
.=
(SubJoin M) . (
(A "\/" B),
C)
by LATTICES:def 1
.=
(A "\/" B) "\/" C
by LATTICES:def 1
;
verum
end;
A15:
for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" (A "\/" B) = A
proof
let A,
B be
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #);
A "/\" (A "\/" B) = A
consider W1 being
strict Subspace of
M such that A16:
W1 = A
by Def3;
consider W2 being
strict Subspace of
M such that A17:
W2 = B
by Def3;
reconsider AB =
W1 + W2 as
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #)
by Def3;
thus A "/\" (A "\/" B) =
(SubMeet M) . (
A,
(A "\/" B))
by LATTICES:def 2
.=
(SubMeet M) . (
A,
((SubJoin M) . (A,B)))
by LATTICES:def 1
.=
(SubMeet M) . (
A,
AB)
by A16, A17, Def7
.=
W1 /\ (W1 + W2)
by A16, Def8
.=
A
by A16, Lm11, VECTSP_4:29
;
verum
end;
for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "\/" B = B "\/" A
then
( LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is join-commutative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is join-associative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is meet-absorbing & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is meet-commutative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is meet-associative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is join-absorbing )
by A11, A4, A1, A7, A15, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
hence
LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice
; verum