Definition df-com2

Description: A device to add commutativity to various sorts of rings. I use ran g because I suppose g has a neutral element and therefore is onto. (Contributed by FL, 6-Sep-2009) (New usage is discouraged.)

	Ref	Expression
Assertion	df-com2	⊢ Com2 = { ⟨ 𝑔 , ℎ ⟩ ∣ ∀ 𝑎 ∈ ran 𝑔 ∀ 𝑏 ∈ ran 𝑔 ( 𝑎 ℎ 𝑏 ) = ( 𝑏 ℎ 𝑎 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccm2	⊢ Com2
1		vg	⊢ 𝑔
2		vh	⊢ ℎ
3		va	⊢ 𝑎
4	1	cv	⊢ 𝑔
5	4	crn	⊢ ran 𝑔
6		vb	⊢ 𝑏
7	3	cv	⊢ 𝑎
8	2	cv	⊢ ℎ
9	6	cv	⊢ 𝑏
10	7 9 8	co	⊢ ( 𝑎 ℎ 𝑏 )
11	9 7 8	co	⊢ ( 𝑏 ℎ 𝑎 )
12	10 11	wceq	⊢ ( 𝑎 ℎ 𝑏 ) = ( 𝑏 ℎ 𝑎 )
13	12 6 5	wral	⊢ ∀ 𝑏 ∈ ran 𝑔 ( 𝑎 ℎ 𝑏 ) = ( 𝑏 ℎ 𝑎 )
14	13 3 5	wral	⊢ ∀ 𝑎 ∈ ran 𝑔 ∀ 𝑏 ∈ ran 𝑔 ( 𝑎 ℎ 𝑏 ) = ( 𝑏 ℎ 𝑎 )
15	14 1 2	copab	⊢ { ⟨ 𝑔 , ℎ ⟩ ∣ ∀ 𝑎 ∈ ran 𝑔 ∀ 𝑏 ∈ ran 𝑔 ( 𝑎 ℎ 𝑏 ) = ( 𝑏 ℎ 𝑎 ) }
16	0 15	wceq	⊢ Com2 = { ⟨ 𝑔 , ℎ ⟩ ∣ ∀ 𝑎 ∈ ran 𝑔 ∀ 𝑏 ∈ ran 𝑔 ( 𝑎 ℎ 𝑏 ) = ( 𝑏 ℎ 𝑎 ) }