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

Metamath Proof Explorer

Theorem cmbr

Description: Binary relation expressing A commutes with B . Definition of commutes in Kalmbach p. 20. (Contributed by NM, 14-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cmbr ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ Cℋ ↔ 𝐴 ∈ Cℋ ) )
2 1 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ↔ ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ) )
3 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
4 ineq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∩ 𝑦 ) = ( 𝐴 ∩ 𝑦 ) )
5 ineq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∩ ( ⊥ ‘ 𝑦 ) ) = ( 𝐴 ∩ ( ⊥ ‘ 𝑦 ) ) )
6 4 5 oveq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∩ 𝑦 ) ∨ℋ ( 𝑥 ∩ ( ⊥ ‘ 𝑦 ) ) ) = ( ( 𝐴 ∩ 𝑦 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝑦 ) ) ) )
7 3 6 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = ( ( 𝑥 ∩ 𝑦 ) ∨ℋ ( 𝑥 ∩ ( ⊥ ‘ 𝑦 ) ) ) ↔ 𝐴 = ( ( 𝐴 ∩ 𝑦 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝑦 ) ) ) ) )
8 2 7 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 = ( ( 𝑥 ∩ 𝑦 ) ∨ℋ ( 𝑥 ∩ ( ⊥ ‘ 𝑦 ) ) ) ) ↔ ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝐴 = ( ( 𝐴 ∩ 𝑦 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝑦 ) ) ) ) ) )
9 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ Cℋ ↔ 𝐵 ∈ Cℋ ) )
10 9 anbi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ↔ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) )
11 ineq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∩ 𝑦 ) = ( 𝐴 ∩ 𝐵 ) )
12 fveq2 ⊢ ( 𝑦 = 𝐵 → ( ⊥ ‘ 𝑦 ) = ( ⊥ ‘ 𝐵 ) )
13 12 ineq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∩ ( ⊥ ‘ 𝑦 ) ) = ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) )
14 11 13 oveq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∩ 𝑦 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝑦 ) ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )
15 14 eqeq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐴 = ( ( 𝐴 ∩ 𝑦 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝑦 ) ) ) ↔ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )
16 10 15 anbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝐴 = ( ( 𝐴 ∩ 𝑦 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝑦 ) ) ) ) ↔ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) )
17 df-cm ⊢ 𝐶ℋ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 = ( ( 𝑥 ∩ 𝑦 ) ∨ℋ ( 𝑥 ∩ ( ⊥ ‘ 𝑦 ) ) ) ) }
18 8 16 17 brabg ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) )
19 18 bianabs ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )