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 𝐺 ( 𝑎 𝐻 𝑏 ) = ( 𝑏 𝐻 𝑎 ) ) )