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

Metamath Proof Explorer

Theorem cmcm

Description: Commutation is symmetric. Theorem 2(v) of Kalmbach p. 22. (Contributed by NM, 13-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion cmcm ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝐶 ℋ B ↔ B 𝐶 ℋ A

Proof

Step Hyp Ref Expression
1 breq1 ⊢ A = if A ∈ C ℋ A 0 ℋ → A 𝐶 ℋ B ↔ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B
2 breq2 ⊢ A = if A ∈ C ℋ A 0 ℋ → B 𝐶 ℋ A ↔ B 𝐶 ℋ if A ∈ C ℋ A 0 ℋ
3 1 2 bibi12d ⊢ A = if A ∈ C ℋ A 0 ℋ → A 𝐶 ℋ B ↔ B 𝐶 ℋ A ↔ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B ↔ B 𝐶 ℋ if A ∈ C ℋ A 0 ℋ
4 breq2 ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B ↔ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ if B ∈ C ℋ B 0 ℋ
5 breq1 ⊢ B = if B ∈ C ℋ B 0 ℋ → B 𝐶 ℋ if A ∈ C ℋ A 0 ℋ ↔ if B ∈ C ℋ B 0 ℋ 𝐶 ℋ if A ∈ C ℋ A 0 ℋ
6 4 5 bibi12d ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B ↔ B 𝐶 ℋ if A ∈ C ℋ A 0 ℋ ↔ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ if B ∈ C ℋ B 0 ℋ ↔ if B ∈ C ℋ B 0 ℋ 𝐶 ℋ if A ∈ C ℋ A 0 ℋ
7 h0elch ⊢ 0 ℋ ∈ C ℋ
8 7 elimel ⊢ if A ∈ C ℋ A 0 ℋ ∈ C ℋ
9 7 elimel ⊢ if B ∈ C ℋ B 0 ℋ ∈ C ℋ
10 8 9 cmcmi ⊢ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ if B ∈ C ℋ B 0 ℋ ↔ if B ∈ C ℋ B 0 ℋ 𝐶 ℋ if A ∈ C ℋ A 0 ℋ
11 3 6 10 dedth2h ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝐶 ℋ B ↔ B 𝐶 ℋ A