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=BaseK
cmt2.o ⊢⊥˙=oc⁡K
cmt2.c ⊢C=cm⁡K
Assertion cmt2N ⊢K∈OML∧X∈B∧Y∈B→XCY↔XC⊥˙⁡Y

Proof

Step Hyp Ref Expression
1 cmt2.b ⊢B=BaseK
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→Xmeet⁡KY∈B
8 4 7 syl3an1 ⊢K∈OML∧X∈B∧Y∈B→Xmeet⁡KY∈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→Xmeet⁡K⊥˙⁡Y∈B
16 5 9 14 15 syl3anc ⊢K∈OML∧X∈B∧Y∈B→Xmeet⁡K⊥˙⁡Y∈B
17 eqid ⊢join⁡K=join⁡K
18 1 17 latjcom ⊢K∈Lat∧Xmeet⁡KY∈B∧Xmeet⁡K⊥˙⁡Y∈B→Xmeet⁡KYjoin⁡KXmeet⁡K⊥˙⁡Y=Xmeet⁡K⊥˙⁡Yjoin⁡KXmeet⁡KY
19 5 8 16 18 syl3anc ⊢K∈OML∧X∈B∧Y∈B→Xmeet⁡KYjoin⁡KXmeet⁡K⊥˙⁡Y=Xmeet⁡K⊥˙⁡Yjoin⁡KXmeet⁡KY
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→Xmeet⁡K⊥˙⁡⊥˙⁡Y=Xmeet⁡KY
23 22 oveq2d ⊢K∈OML∧X∈B∧Y∈B→Xmeet⁡K⊥˙⁡Yjoin⁡KXmeet⁡K⊥˙⁡⊥˙⁡Y=Xmeet⁡K⊥˙⁡Yjoin⁡KXmeet⁡KY
24 19 23 eqtr4d ⊢K∈OML∧X∈B∧Y∈B→Xmeet⁡KYjoin⁡KXmeet⁡K⊥˙⁡Y=Xmeet⁡K⊥˙⁡Yjoin⁡KXmeet⁡K⊥˙⁡⊥˙⁡Y
25 24 eqeq2d ⊢K∈OML∧X∈B∧Y∈B→X=Xmeet⁡KYjoin⁡KXmeet⁡K⊥˙⁡Y↔X=Xmeet⁡K⊥˙⁡Yjoin⁡KXmeet⁡K⊥˙⁡⊥˙⁡Y
26 1 17 6 2 3 cmtvalN ⊢K∈OML∧X∈B∧Y∈B→XCY↔X=Xmeet⁡KYjoin⁡KXmeet⁡K⊥˙⁡Y
27 1 17 6 2 3 cmtvalN ⊢K∈OML∧X∈B∧⊥˙⁡Y∈B→XC⊥˙⁡Y↔X=Xmeet⁡K⊥˙⁡Yjoin⁡KXmeet⁡K⊥˙⁡⊥˙⁡Y
28 14 27 syld3an3 ⊢K∈OML∧X∈B∧Y∈B→XC⊥˙⁡Y↔X=Xmeet⁡K⊥˙⁡Yjoin⁡KXmeet⁡K⊥˙⁡⊥˙⁡Y
29 25 26 28 3bitr4d ⊢K∈OML∧X∈B∧Y∈B→XCY↔XC⊥˙⁡Y