let V be RealUnitarySpace; :: thesis: 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, 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) #);
:: thesis: 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
;
:: thesis: verum
end;
A3:
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) #);
:: thesis: (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
;
:: thesis: verum
end;
A4:
for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" B = B "/\" A
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) #);
:: thesis: 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
;
:: thesis: verum
end;
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) #);
:: thesis: 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
;
:: thesis: verum
end;
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 A1, A2, A3, A4, A5, 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
; :: thesis: verum