Metamath Proof Explorer

Theorem cmt3N

Description: Commutation with orthocomplement. Remark in Kalmbach p. 23. ( cmcm4i 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 cmt3N ⊢ 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 1 2 3 cmt2N ⊢ K ∈ OML ∧ Y ∈ B ∧ X ∈ B → Y C X ↔ Y C ⊥ ˙ ⁡ X
5 4 3com23 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → Y C X ↔ Y C ⊥ ˙ ⁡ X
6 1 3 cmtcomN ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X C Y ↔ Y C X
7 omlop ⊢ K ∈ OML → K ∈ OP
8 7 3ad2ant1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → K ∈ OP
9 simp2 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X ∈ B
10 1 2 opoccl ⊢ K ∈ OP ∧ X ∈ B → ⊥ ˙ ⁡ X ∈ B
11 8 9 10 syl2anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → ⊥ ˙ ⁡ X ∈ B
12 1 3 cmtcomN ⊢ K ∈ OML ∧ ⊥ ˙ ⁡ X ∈ B ∧ Y ∈ B → ⊥ ˙ ⁡ X C Y ↔ Y C ⊥ ˙ ⁡ X
13 11 12 syld3an2 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → ⊥ ˙ ⁡ X C Y ↔ Y C ⊥ ˙ ⁡ X
14 5 6 13 3bitr4d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X C Y ↔ ⊥ ˙ ⁡ X C Y