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

Definition df-rngo 35054
Description: Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-rngo RingOps = {⟨𝑔, ⟩ ∣ ((𝑔 ∈ AbelOp ∧ :(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ∧ ∃𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦)))}
Distinct variable group:   𝑔,,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-rngo
StepHypRef Expression
1 crngo 35053 . 2 class RingOps
2 vg . . . . . . 7 setvar 𝑔
32cv 1527 . . . . . 6 class 𝑔
4 cablo 28248 . . . . . 6 class AbelOp
53, 4wcel 2105 . . . . 5 wff 𝑔 ∈ AbelOp
63crn 5549 . . . . . . 7 class ran 𝑔
76, 6cxp 5546 . . . . . 6 class (ran 𝑔 × ran 𝑔)
8 vh . . . . . . 7 setvar
98cv 1527 . . . . . 6 class
107, 6, 9wf 6344 . . . . 5 wff :(ran 𝑔 × ran 𝑔)⟶ran 𝑔
115, 10wa 396 . . . 4 wff (𝑔 ∈ AbelOp ∧ :(ran 𝑔 × ran 𝑔)⟶ran 𝑔)
12 vx . . . . . . . . . . . . 13 setvar 𝑥
1312cv 1527 . . . . . . . . . . . 12 class 𝑥
14 vy . . . . . . . . . . . . 13 setvar 𝑦
1514cv 1527 . . . . . . . . . . . 12 class 𝑦
1613, 15, 9co 7145 . . . . . . . . . . 11 class (𝑥𝑦)
17 vz . . . . . . . . . . . 12 setvar 𝑧
1817cv 1527 . . . . . . . . . . 11 class 𝑧
1916, 18, 9co 7145 . . . . . . . . . 10 class ((𝑥𝑦)𝑧)
2015, 18, 9co 7145 . . . . . . . . . . 11 class (𝑦𝑧)
2113, 20, 9co 7145 . . . . . . . . . 10 class (𝑥(𝑦𝑧))
2219, 21wceq 1528 . . . . . . . . 9 wff ((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧))
2315, 18, 3co 7145 . . . . . . . . . . 11 class (𝑦𝑔𝑧)
2413, 23, 9co 7145 . . . . . . . . . 10 class (𝑥(𝑦𝑔𝑧))
2513, 18, 9co 7145 . . . . . . . . . . 11 class (𝑥𝑧)
2616, 25, 3co 7145 . . . . . . . . . 10 class ((𝑥𝑦)𝑔(𝑥𝑧))
2724, 26wceq 1528 . . . . . . . . 9 wff (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧))
2813, 15, 3co 7145 . . . . . . . . . . 11 class (𝑥𝑔𝑦)
2928, 18, 9co 7145 . . . . . . . . . 10 class ((𝑥𝑔𝑦)𝑧)
3025, 20, 3co 7145 . . . . . . . . . 10 class ((𝑥𝑧)𝑔(𝑦𝑧))
3129, 30wceq 1528 . . . . . . . . 9 wff ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))
3222, 27, 31w3a 1079 . . . . . . . 8 wff (((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧)))
3332, 17, 6wral 3135 . . . . . . 7 wff 𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧)))
3433, 14, 6wral 3135 . . . . . 6 wff 𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧)))
3534, 12, 6wral 3135 . . . . 5 wff 𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧)))
3616, 15wceq 1528 . . . . . . . 8 wff (𝑥𝑦) = 𝑦
3715, 13, 9co 7145 . . . . . . . . 9 class (𝑦𝑥)
3837, 15wceq 1528 . . . . . . . 8 wff (𝑦𝑥) = 𝑦
3936, 38wa 396 . . . . . . 7 wff ((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦)
4039, 14, 6wral 3135 . . . . . 6 wff 𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦)
4140, 12, 6wrex 3136 . . . . 5 wff 𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦)
4235, 41wa 396 . . . 4 wff (∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ∧ ∃𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦))
4311, 42wa 396 . . 3 wff ((𝑔 ∈ AbelOp ∧ :(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ∧ ∃𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦)))
4443, 2, 8copab 5119 . 2 class {⟨𝑔, ⟩ ∣ ((𝑔 ∈ AbelOp ∧ :(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ∧ ∃𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦)))}
451, 44wceq 1528 1 wff RingOps = {⟨𝑔, ⟩ ∣ ((𝑔 ∈ AbelOp ∧ :(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ∧ ∃𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦)))}
Colors of variables: wff setvar class
This definition is referenced by:  relrngo  35055  isrngo  35056
  Copyright terms: Public domain W3C validator