let V be RealLinearSpace; 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 =
A "\/" C
by Def7
.=
W3
by A1, LATTICES:def 3
;
then A2:
W1 is
Subspace of
W3
by Th12;
thus A "\/" (B "/\" C) =
(SubJoin V) . A,
BC
by Def8
.=
W1 + (W2 /\ W3)
by Def7
.=
(W1 + W2) /\ W3
by A2, Th33
.=
(SubMeet V) . AB,
C
by Def8
.=
(A "\/" B) "/\" C
by Def7
;
verum
end;
hence
LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular
by LATTICES:def 12; verum