let V be RealLinearSpace; :: thesis: 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

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

hence
LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular
; :: thesis: verum
let A, B, C be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); :: thesis: ( 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 ; :: thesis: 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 ;

then A2: W1 is Subspace of W3 by Th8;

thus A "\/" (B "/\" C) = (SubJoin V) . (A,BC) by Def8

.= W1 + (W2 /\ W3) by Def7

.= (W1 + W2) /\ W3 by A2, Th29

.= (SubMeet V) . (AB,C) by Def8

.= (A "\/" B) "/\" C by Def7 ; :: thesis: verum

end;reconsider W1 = A, W2 = B, W3 = C as strict Subspace of V by Def3;

assume A1: A [= C ; :: thesis: 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 ;

then A2: W1 is Subspace of W3 by Th8;

thus A "\/" (B "/\" C) = (SubJoin V) . (A,BC) by Def8

.= W1 + (W2 /\ W3) by Def7

.= (W1 + W2) /\ W3 by A2, Th29

.= (SubMeet V) . (AB,C) by Def8

.= (A "\/" B) "/\" C by Def7 ; :: thesis: verum