let V be RealUnitarySpace; LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular
set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #);
for A, B, C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) st A [= C holds
A "\/" (B "/\" C) = (A "\/" B) "/\" C
proof
let A,
B,
C be
Element of
LattStr(#
(Subspaces V),
(SubJoin V),
(SubMeet V) #);
( A [= C implies A "\/" (B "/\" C) = (A "\/" B) "/\" C )
reconsider W1 =
A,
W2 =
B,
W3 =
C as
strict Subspace of
V by Def3;
assume A1:
A [= C
;
A "\/" (B "/\" C) = (A "\/" B) "/\" C
reconsider AB =
W1 + W2 as
Element of
LattStr(#
(Subspaces V),
(SubJoin V),
(SubMeet V) #)
by Def3;
reconsider BC =
W2 /\ W3 as
Element of
LattStr(#
(Subspaces V),
(SubJoin V),
(SubMeet V) #)
by Def3;
W1 + W3 =
(SubJoin V) . (
A,
C)
by Def7
.=
A "\/" C
by LATTICES:def 1
.=
W3
by A1, LATTICES:def 3
;
then A2:
W1 is
Subspace of
W3
by Th8;
thus A "\/" (B "/\" C) =
(SubJoin V) . (
A,
(B "/\" C))
by LATTICES:def 1
.=
(SubJoin V) . (
A,
((SubMeet V) . (B,C)))
by LATTICES:def 2
.=
(SubJoin V) . (
A,
BC)
by Def8
.=
W1 + (W2 /\ W3)
by Def7
.=
(W1 + W2) /\ W3
by A2, Th29
.=
(SubMeet V) . (
AB,
C)
by Def8
.=
(SubMeet V) . (
((SubJoin V) . (A,B)),
C)
by Def7
.=
(SubMeet V) . (
(A "\/" B),
C)
by LATTICES:def 1
.=
(A "\/" B) "/\" C
by LATTICES:def 2
;
verum
end;
hence
LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular
by LATTICES:def 12; verum