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 ⊢ 𝐴 ∈ Cℋ
pjoml2.2 ⊢ 𝐵 ∈ Cℋ
Assertion cmcm3i ( 𝐴 𝐶ℋ 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐵 )

Proof

Step Hyp Ref Expression
1 pjoml2.1 ⊢ 𝐴 ∈ Cℋ
2 pjoml2.2 ⊢ 𝐵 ∈ Cℋ
3 2 1 cmcm2i ⊢ ( 𝐵 𝐶ℋ 𝐴 ↔ 𝐵 𝐶ℋ ( ⊥ ‘ 𝐴 ) )
4 1 2 cmcmi ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴 )
5 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
6 5 2 cmcmi ⊢ ( ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ ( ⊥ ‘ 𝐴 ) )
7 3 4 6 3bitr4i ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐵 )