This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmcm3i

Description: Commutation with orthocomplement. Remark in Kalmbach p. 23. (Contributed by NM, 4-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 ⊢ A ∈ C ℋ
pjoml2.2 ⊢ B ∈ C ℋ
Assertion cmcm3i ⊢ A 𝐶 ℋ B ↔ ⊥ ⁡ A 𝐶 ℋ B

Proof

Step Hyp Ref Expression
1 pjoml2.1 ⊢ A ∈ C ℋ
2 pjoml2.2 ⊢ B ∈ C ℋ
3 2 1 cmcm2i ⊢ B 𝐶 ℋ A ↔ B 𝐶 ℋ ⊥ ⁡ A
4 1 2 cmcmi ⊢ A 𝐶 ℋ B ↔ B 𝐶 ℋ A
5 1 choccli ⊢ ⊥ ⁡ A ∈ C ℋ
6 5 2 cmcmi ⊢ ⊥ ⁡ A 𝐶 ℋ B ↔ B 𝐶 ℋ ⊥ ⁡ A
7 3 4 6 3bitr4i ⊢ A 𝐶 ℋ B ↔ ⊥ ⁡ A 𝐶 ℋ B