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

Metamath Proof Explorer

Theorem cmbr3

Description: Alternate definition for the commutes relation. Lemma 3 of Kalmbach p. 23. (Contributed by NM, 14-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion cmbr3 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝐶 ℋ B ↔ A ∩ ⊥ ⁡ A ∨ ℋ B = A ∩ B

Proof

Step Hyp Ref Expression
1 breq1 ⊢ A = if A ∈ C ℋ A 0 ℋ → A 𝐶 ℋ B ↔ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B
2 id ⊢ A = if A ∈ C ℋ A 0 ℋ → A = if A ∈ C ℋ A 0 ℋ
3 fveq2 ⊢ A = if A ∈ C ℋ A 0 ℋ → ⊥ ⁡ A = ⊥ ⁡ if A ∈ C ℋ A 0 ℋ
4 3 oveq1d ⊢ A = if A ∈ C ℋ A 0 ℋ → ⊥ ⁡ A ∨ ℋ B = ⊥ ⁡ if A ∈ C ℋ A 0 ℋ ∨ ℋ B
5 2 4 ineq12d ⊢ A = if A ∈ C ℋ A 0 ℋ → A ∩ ⊥ ⁡ A ∨ ℋ B = if A ∈ C ℋ A 0 ℋ ∩ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ ∨ ℋ B
6 ineq1 ⊢ A = if A ∈ C ℋ A 0 ℋ → A ∩ B = if A ∈ C ℋ A 0 ℋ ∩ B
7 5 6 eqeq12d ⊢ A = if A ∈ C ℋ A 0 ℋ → A ∩ ⊥ ⁡ A ∨ ℋ B = A ∩ B ↔ if A ∈ C ℋ A 0 ℋ ∩ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ ∨ ℋ B = if A ∈ C ℋ A 0 ℋ ∩ B
8 1 7 bibi12d ⊢ A = if A ∈ C ℋ A 0 ℋ → A 𝐶 ℋ B ↔ A ∩ ⊥ ⁡ A ∨ ℋ B = A ∩ B ↔ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B ↔ if A ∈ C ℋ A 0 ℋ ∩ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ ∨ ℋ B = if A ∈ C ℋ A 0 ℋ ∩ B
9 breq2 ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B ↔ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ if B ∈ C ℋ B 0 ℋ
10 oveq2 ⊢ B = if B ∈ C ℋ B 0 ℋ → ⊥ ⁡ if A ∈ C ℋ A 0 ℋ ∨ ℋ B = ⊥ ⁡ if A ∈ C ℋ A 0 ℋ ∨ ℋ if B ∈ C ℋ B 0 ℋ
11 10 ineq2d ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ ∩ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ ∨ ℋ B = if A ∈ C ℋ A 0 ℋ ∩ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ ∨ ℋ if B ∈ C ℋ B 0 ℋ
12 ineq2 ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ ∩ B = if A ∈ C ℋ A 0 ℋ ∩ if B ∈ C ℋ B 0 ℋ
13 11 12 eqeq12d ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ ∩ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ ∨ ℋ B = if A ∈ C ℋ A 0 ℋ ∩ B ↔ if A ∈ C ℋ A 0 ℋ ∩ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ ∨ ℋ if B ∈ C ℋ B 0 ℋ = if A ∈ C ℋ A 0 ℋ ∩ if B ∈ C ℋ B 0 ℋ
14 9 13 bibi12d ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B ↔ if A ∈ C ℋ A 0 ℋ ∩ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ ∨ ℋ B = if A ∈ C ℋ A 0 ℋ ∩ B ↔ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ if B ∈ C ℋ B 0 ℋ ↔ if A ∈ C ℋ A 0 ℋ ∩ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ ∨ ℋ if B ∈ C ℋ B 0 ℋ = if A ∈ C ℋ A 0 ℋ ∩ if B ∈ C ℋ B 0 ℋ
15 h0elch ⊢ 0 ℋ ∈ C ℋ
16 15 elimel ⊢ if A ∈ C ℋ A 0 ℋ ∈ C ℋ
17 15 elimel ⊢ if B ∈ C ℋ B 0 ℋ ∈ C ℋ
18 16 17 cmbr3i ⊢ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ if B ∈ C ℋ B 0 ℋ ↔ if A ∈ C ℋ A 0 ℋ ∩ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ ∨ ℋ if B ∈ C ℋ B 0 ℋ = if A ∈ C ℋ A 0 ℋ ∩ if B ∈ C ℋ B 0 ℋ
19 8 14 18 dedth2h ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝐶 ℋ B ↔ A ∩ ⊥ ⁡ A ∨ ℋ B = A ∩ B