Users' Mathboxes 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 35760
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 35759 . 2 class Com2
2 va . . . . . . . 8 setvar 𝑎
32cv 1541 . . . . . . 7 class 𝑎
4 vb . . . . . . . 8 setvar 𝑏
54cv 1541 . . . . . . 7 class 𝑏
6 vh . . . . . . . 8 setvar
76cv 1541 . . . . . . 7 class
83, 5, 7co 7164 . . . . . 6 class (𝑎𝑏)
95, 3, 7co 7164 . . . . . 6 class (𝑏𝑎)
108, 9wceq 1542 . . . . 5 wff (𝑎𝑏) = (𝑏𝑎)
11 vg . . . . . . 7 setvar 𝑔
1211cv 1541 . . . . . 6 class 𝑔
1312crn 5520 . . . . 5 class ran 𝑔
1410, 4, 13wral 3053 . . . 4 wff 𝑏 ∈ ran 𝑔(𝑎𝑏) = (𝑏𝑎)
1514, 2, 13wral 3053 . . 3 wff 𝑎 ∈ ran 𝑔𝑏 ∈ ran 𝑔(𝑎𝑏) = (𝑏𝑎)
1615, 11, 6copab 5089 . 2 class {⟨𝑔, ⟩ ∣ ∀𝑎 ∈ ran 𝑔𝑏 ∈ ran 𝑔(𝑎𝑏) = (𝑏𝑎)}
171, 16wceq 1542 1 wff Com2 = {⟨𝑔, ⟩ ∣ ∀𝑎 ∈ ran 𝑔𝑏 ∈ ran 𝑔(𝑎𝑏) = (𝑏𝑎)}
Colors of variables: wff setvar class
This definition is referenced by:  iscom2  35765
  Copyright terms: Public domain W3C validator