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ℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )