Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-com2 Structured version   Visualization version   GIF version

Definition df-com2 32959
 Description: A device to add commutativity to various sorts of rings. I use ran 𝑔 because I suppose 𝑔 has a neutral element and therefore is onto. (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.)
Assertion
Ref Expression
df-com2 Com2 = {⟨𝑔, ⟩ ∣ ∀𝑎 ∈ ran 𝑔𝑏 ∈ ran 𝑔(𝑎𝑏) = (𝑏𝑎)}
Distinct variable group:   𝑔,,𝑎,𝑏

Detailed syntax breakdown of Definition df-com2
StepHypRef Expression
1 ccm2 32958 . 2 class Com2
2 va . . . . . . . 8 setvar 𝑎
32cv 1474 . . . . . . 7 class 𝑎
4 vb . . . . . . . 8 setvar 𝑏
54cv 1474 . . . . . . 7 class 𝑏
6 vh . . . . . . . 8 setvar
76cv 1474 . . . . . . 7 class
83, 5, 7co 6549 . . . . . 6 class (𝑎𝑏)
95, 3, 7co 6549 . . . . . 6 class (𝑏𝑎)
108, 9wceq 1475 . . . . 5 wff (𝑎𝑏) = (𝑏𝑎)
11 vg . . . . . . 7 setvar 𝑔
1211cv 1474 . . . . . 6 class 𝑔
1312crn 5039 . . . . 5 class ran 𝑔
1410, 4, 13wral 2896 . . . 4 wff 𝑏 ∈ ran 𝑔(𝑎𝑏) = (𝑏𝑎)
1514, 2, 13wral 2896 . . 3 wff 𝑎 ∈ ran 𝑔𝑏 ∈ ran 𝑔(𝑎𝑏) = (𝑏𝑎)
1615, 11, 6copab 4642 . 2 class {⟨𝑔, ⟩ ∣ ∀𝑎 ∈ ran 𝑔𝑏 ∈ ran 𝑔(𝑎𝑏) = (𝑏𝑎)}
171, 16wceq 1475 1 wff Com2 = {⟨𝑔, ⟩ ∣ ∀𝑎 ∈ ran 𝑔𝑏 ∈ ran 𝑔(𝑎𝑏) = (𝑏𝑎)}
 Colors of variables: wff setvar class This definition is referenced by:  iscom2  32964
 Copyright terms: Public domain W3C validator