Metamath Proof Explorer


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 𝑔 ( 𝑎 𝑏 ) = ( 𝑏 𝑎 ) }