let V be RealUnitarySpace; LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice
set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #);
A1:
for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" B = B "/\" A
A2:
for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds (A "/\" B) "\/" B = B
proof
let A,
B be
Element of
LattStr(#
(Subspaces V),
(SubJoin V),
(SubMeet V) #);
(A "/\" B) "\/" B = B
reconsider W1 =
A,
W2 =
B as
strict Subspace of
V by Def3;
reconsider AB =
W1 /\ W2 as
Element of
LattStr(#
(Subspaces V),
(SubJoin V),
(SubMeet V) #)
by Def3;
thus (A "/\" B) "\/" B =
(SubJoin V) . (
(A "/\" B),
B)
by LATTICES:def 1
.=
(SubJoin V) . (
((SubMeet V) . (A,B)),
B)
by LATTICES:def 2
.=
(SubJoin V) . (
AB,
B)
by Def8
.=
(W1 /\ W2) + W2
by Def7
.=
B
by Lm6, RUSUB_1:24
;
verum
end;
A3:
for A, B, C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "\/" (B "\/" C) = (A "\/" B) "\/" C
proof
let A,
B,
C be
Element of
LattStr(#
(Subspaces V),
(SubJoin V),
(SubMeet V) #);
A "\/" (B "\/" C) = (A "\/" B) "\/" C
reconsider W1 =
A,
W2 =
B,
W3 =
C as
Subspace of
V by Def3;
reconsider AB =
W1 + W2,
BC =
W2 + W3 as
Element of
LattStr(#
(Subspaces V),
(SubJoin V),
(SubMeet V) #)
by Def3;
thus A "\/" (B "\/" C) =
(SubJoin V) . (
A,
(B "\/" C))
by LATTICES:def 1
.=
(SubJoin V) . (
A,
((SubJoin V) . (B,C)))
by LATTICES:def 1
.=
(SubJoin V) . (
A,
BC)
by Def7
.=
W1 + (W2 + W3)
by Def7
.=
(W1 + W2) + W3
by Th6
.=
(SubJoin V) . (
AB,
C)
by Def7
.=
(SubJoin V) . (
((SubJoin V) . (A,B)),
C)
by Def7
.=
(SubJoin V) . (
(A "\/" B),
C)
by LATTICES:def 1
.=
(A "\/" B) "\/" C
by LATTICES:def 1
;
verum
end;
A4:
for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" (A "\/" B) = A
proof
let A,
B be
Element of
LattStr(#
(Subspaces V),
(SubJoin V),
(SubMeet V) #);
A "/\" (A "\/" B) = A
reconsider W1 =
A,
W2 =
B as
strict Subspace of
V by Def3;
reconsider AB =
W1 + W2 as
Element of
LattStr(#
(Subspaces V),
(SubJoin V),
(SubMeet V) #)
by Def3;
thus A "/\" (A "\/" B) =
(SubMeet V) . (
A,
(A "\/" B))
by LATTICES:def 2
.=
(SubMeet V) . (
A,
((SubJoin V) . (A,B)))
by LATTICES:def 1
.=
(SubMeet V) . (
A,
AB)
by Def7
.=
W1 /\ (W1 + W2)
by Def8
.=
A
by Lm7, RUSUB_1:24
;
verum
end;
A5:
for A, B, C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" (B "/\" C) = (A "/\" B) "/\" C
proof
let A,
B,
C be
Element of
LattStr(#
(Subspaces V),
(SubJoin V),
(SubMeet V) #);
A "/\" (B "/\" C) = (A "/\" B) "/\" C
reconsider W1 =
A,
W2 =
B,
W3 =
C as
Subspace of
V by Def3;
reconsider AB =
W1 /\ W2,
BC =
W2 /\ W3 as
Element of
LattStr(#
(Subspaces V),
(SubJoin V),
(SubMeet V) #)
by Def3;
thus A "/\" (B "/\" C) =
(SubMeet V) . (
A,
(B "/\" C))
by LATTICES:def 2
.=
(SubMeet V) . (
A,
((SubMeet V) . (B,C)))
by LATTICES:def 2
.=
(SubMeet V) . (
A,
BC)
by Def8
.=
W1 /\ (W2 /\ W3)
by Def8
.=
(W1 /\ W2) /\ W3
by Th15
.=
(SubMeet V) . (
AB,
C)
by Def8
.=
(SubMeet V) . (
((SubMeet V) . (A,B)),
C)
by Def8
.=
(SubMeet V) . (
(A "/\" B),
C)
by LATTICES:def 2
.=
(A "/\" B) "/\" C
by LATTICES:def 2
;
verum
end;
for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "\/" B = B "\/" A
then
( LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is join-commutative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is join-associative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is meet-absorbing & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is meet-commutative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is meet-associative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is join-absorbing )
by A3, A2, A1, A5, A4, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
hence
LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice
; verum