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

Metamath Proof Explorer

Theorem iscom2

Description: A device to add commutativity to various sorts of rings. (Contributed by FL, 6-Sep-2009) (New usage is discouraged.)

Ref Expression
Assertion iscom2 ( ( 𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐵 ) → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ Com2 ↔ ∀ 𝑎 ∈ ran 𝐺 ∀ 𝑏 ∈ ran 𝐺 ( 𝑎 𝐻 𝑏 ) = ( 𝑏 𝐻 𝑎 ) ) )

Proof

Step Hyp Ref Expression
1 df-com2 ⊢ Com2 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∀ 𝑎 ∈ ran 𝑥 ∀ 𝑏 ∈ ran 𝑥 ( 𝑎 𝑦 𝑏 ) = ( 𝑏 𝑦 𝑎 ) }
2 1 a1i ⊢ ( ( 𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐵 ) → Com2 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∀ 𝑎 ∈ ran 𝑥 ∀ 𝑏 ∈ ran 𝑥 ( 𝑎 𝑦 𝑏 ) = ( 𝑏 𝑦 𝑎 ) } )
3 2 eleq2d ⊢ ( ( 𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐵 ) → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ Com2 ↔ ⟨ 𝐺 , 𝐻 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∀ 𝑎 ∈ ran 𝑥 ∀ 𝑏 ∈ ran 𝑥 ( 𝑎 𝑦 𝑏 ) = ( 𝑏 𝑦 𝑎 ) } ) )
4 rneq ⊢ ( 𝑥 = 𝐺 → ran 𝑥 = ran 𝐺 )
5 4 raleqdv ⊢ ( 𝑥 = 𝐺 → ( ∀ 𝑏 ∈ ran 𝑥 ( 𝑎 𝑦 𝑏 ) = ( 𝑏 𝑦 𝑎 ) ↔ ∀ 𝑏 ∈ ran 𝐺 ( 𝑎 𝑦 𝑏 ) = ( 𝑏 𝑦 𝑎 ) ) )
6 4 5 raleqbidv ⊢ ( 𝑥 = 𝐺 → ( ∀ 𝑎 ∈ ran 𝑥 ∀ 𝑏 ∈ ran 𝑥 ( 𝑎 𝑦 𝑏 ) = ( 𝑏 𝑦 𝑎 ) ↔ ∀ 𝑎 ∈ ran 𝐺 ∀ 𝑏 ∈ ran 𝐺 ( 𝑎 𝑦 𝑏 ) = ( 𝑏 𝑦 𝑎 ) ) )
7 oveq ⊢ ( 𝑦 = 𝐻 → ( 𝑎 𝑦 𝑏 ) = ( 𝑎 𝐻 𝑏 ) )
8 oveq ⊢ ( 𝑦 = 𝐻 → ( 𝑏 𝑦 𝑎 ) = ( 𝑏 𝐻 𝑎 ) )
9 7 8 eqeq12d ⊢ ( 𝑦 = 𝐻 → ( ( 𝑎 𝑦 𝑏 ) = ( 𝑏 𝑦 𝑎 ) ↔ ( 𝑎 𝐻 𝑏 ) = ( 𝑏 𝐻 𝑎 ) ) )
10 9 2ralbidv ⊢ ( 𝑦 = 𝐻 → ( ∀ 𝑎 ∈ ran 𝐺 ∀ 𝑏 ∈ ran 𝐺 ( 𝑎 𝑦 𝑏 ) = ( 𝑏 𝑦 𝑎 ) ↔ ∀ 𝑎 ∈ ran 𝐺 ∀ 𝑏 ∈ ran 𝐺 ( 𝑎 𝐻 𝑏 ) = ( 𝑏 𝐻 𝑎 ) ) )
11 6 10 opelopabg ⊢ ( ( 𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐵 ) → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∀ 𝑎 ∈ ran 𝑥 ∀ 𝑏 ∈ ran 𝑥 ( 𝑎 𝑦 𝑏 ) = ( 𝑏 𝑦 𝑎 ) } ↔ ∀ 𝑎 ∈ ran 𝐺 ∀ 𝑏 ∈ ran 𝐺 ( 𝑎 𝐻 𝑏 ) = ( 𝑏 𝐻 𝑎 ) ) )
12 3 11 bitrd ⊢ ( ( 𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐵 ) → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ Com2 ↔ ∀ 𝑎 ∈ ran 𝐺 ∀ 𝑏 ∈ ran 𝐺 ( 𝑎 𝐻 𝑏 ) = ( 𝑏 𝐻 𝑎 ) ) )