Metamath Proof Explorer

Theorem cmt4N

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 cmt4N ⊢ 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 ∧ X ∈ B ∧ Y ∈ B → X C Y ↔ X C ⊥ ˙ ⁡ Y
5 omlop ⊢ K ∈ OML → K ∈ OP
6 5 3ad2ant1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → K ∈ OP
7 simp3 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
8 1 2 opoccl ⊢ K ∈ OP ∧ Y ∈ B → ⊥ ˙ ⁡ Y ∈ B
9 6 7 8 syl2anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → ⊥ ˙ ⁡ Y ∈ B
10 1 2 3 cmt3N ⊢ K ∈ OML ∧ X ∈ B ∧ ⊥ ˙ ⁡ Y ∈ B → X C ⊥ ˙ ⁡ Y ↔ ⊥ ˙ ⁡ X C ⊥ ˙ ⁡ Y
11 9 10 syld3an3 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X C ⊥ ˙ ⁡ Y ↔ ⊥ ˙ ⁡ X C ⊥ ˙ ⁡ Y
12 4 11 bitrd ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X C Y ↔ ⊥ ˙ ⁡ X C ⊥ ˙ ⁡ Y