Metamath Proof Explorer


Theorem cmt2N

Description: Commutation with orthocomplement. Theorem 2.3(i) of Beran p. 39. ( cmcm2i analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses cmt2.b B = Base K
cmt2.o ˙ = oc K
cmt2.c C = cm K
Assertion cmt2N K OML X B Y B X C Y X C ˙ Y

Proof

Step Hyp Ref Expression
1 cmt2.b B = Base K
2 cmt2.o ˙ = oc K
3 cmt2.c C = cm K
4 omllat K OML K Lat
5 4 3ad2ant1 K OML X B Y B K Lat
6 eqid meet K = meet K
7 1 6 latmcl K Lat X B Y B X meet K Y B
8 4 7 syl3an1 K OML X B Y B X meet K Y B
9 simp2 K OML X B Y B X B
10 omlop K OML K OP
11 10 3ad2ant1 K OML X B Y B K OP
12 simp3 K OML X B Y B Y B
13 1 2 opoccl K OP Y B ˙ Y B
14 11 12 13 syl2anc K OML X B Y B ˙ Y B
15 1 6 latmcl K Lat X B ˙ Y B X meet K ˙ Y B
16 5 9 14 15 syl3anc K OML X B Y B X meet K ˙ Y B
17 eqid join K = join K
18 1 17 latjcom K Lat X meet K Y B X meet K ˙ Y B X meet K Y join K X meet K ˙ Y = X meet K ˙ Y join K X meet K Y
19 5 8 16 18 syl3anc K OML X B Y B X meet K Y join K X meet K ˙ Y = X meet K ˙ Y join K X meet K Y
20 1 2 opococ K OP Y B ˙ ˙ Y = Y
21 11 12 20 syl2anc K OML X B Y B ˙ ˙ Y = Y
22 21 oveq2d K OML X B Y B X meet K ˙ ˙ Y = X meet K Y
23 22 oveq2d K OML X B Y B X meet K ˙ Y join K X meet K ˙ ˙ Y = X meet K ˙ Y join K X meet K Y
24 19 23 eqtr4d K OML X B Y B X meet K Y join K X meet K ˙ Y = X meet K ˙ Y join K X meet K ˙ ˙ Y
25 24 eqeq2d K OML X B Y B X = X meet K Y join K X meet K ˙ Y X = X meet K ˙ Y join K X meet K ˙ ˙ Y
26 1 17 6 2 3 cmtvalN K OML X B Y B X C Y X = X meet K Y join K X meet K ˙ Y
27 1 17 6 2 3 cmtvalN K OML X B ˙ Y B X C ˙ Y X = X meet K ˙ Y join K X meet K ˙ ˙ Y
28 14 27 syld3an3 K OML X B Y B X C ˙ Y X = X meet K ˙ Y join K X meet K ˙ ˙ Y
29 25 26 28 3bitr4d K OML X B Y B X C Y X C ˙ Y