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