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 36758
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 36757 . 2 class RingOps
2 vg . . . . . . 7 setvar 𝑔
32cv 1540 . . . . . 6 class 𝑔
4 cablo 29792 . . . . . 6 class AbelOp
53, 4wcel 2106 . . . . 5 wff 𝑔 ∈ AbelOp
63crn 5677 . . . . . . 7 class ran 𝑔
76, 6cxp 5674 . . . . . 6 class (ran 𝑔 Γ— ran 𝑔)
8 vh . . . . . . 7 setvar β„Ž
98cv 1540 . . . . . 6 class β„Ž
107, 6, 9wf 6539 . . . . 5 wff β„Ž:(ran 𝑔 Γ— ran 𝑔)⟢ran 𝑔
115, 10wa 396 . . . 4 wff (𝑔 ∈ AbelOp ∧ β„Ž:(ran 𝑔 Γ— ran 𝑔)⟢ran 𝑔)
12 vx . . . . . . . . . . . . 13 setvar π‘₯
1312cv 1540 . . . . . . . . . . . 12 class π‘₯
14 vy . . . . . . . . . . . . 13 setvar 𝑦
1514cv 1540 . . . . . . . . . . . 12 class 𝑦
1613, 15, 9co 7408 . . . . . . . . . . 11 class (π‘₯β„Žπ‘¦)
17 vz . . . . . . . . . . . 12 setvar 𝑧
1817cv 1540 . . . . . . . . . . 11 class 𝑧
1916, 18, 9co 7408 . . . . . . . . . 10 class ((π‘₯β„Žπ‘¦)β„Žπ‘§)
2015, 18, 9co 7408 . . . . . . . . . . 11 class (π‘¦β„Žπ‘§)
2113, 20, 9co 7408 . . . . . . . . . 10 class (π‘₯β„Ž(π‘¦β„Žπ‘§))
2219, 21wceq 1541 . . . . . . . . 9 wff ((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§))
2315, 18, 3co 7408 . . . . . . . . . . 11 class (𝑦𝑔𝑧)
2413, 23, 9co 7408 . . . . . . . . . 10 class (π‘₯β„Ž(𝑦𝑔𝑧))
2513, 18, 9co 7408 . . . . . . . . . . 11 class (π‘₯β„Žπ‘§)
2616, 25, 3co 7408 . . . . . . . . . 10 class ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§))
2724, 26wceq 1541 . . . . . . . . 9 wff (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§))
2813, 15, 3co 7408 . . . . . . . . . . 11 class (π‘₯𝑔𝑦)
2928, 18, 9co 7408 . . . . . . . . . 10 class ((π‘₯𝑔𝑦)β„Žπ‘§)
3025, 20, 3co 7408 . . . . . . . . . 10 class ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§))
3129, 30wceq 1541 . . . . . . . . 9 wff ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§))
3222, 27, 31w3a 1087 . . . . . . . 8 wff (((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§)))
3332, 17, 6wral 3061 . . . . . . 7 wff βˆ€π‘§ ∈ ran 𝑔(((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§)))
3433, 14, 6wral 3061 . . . . . 6 wff βˆ€π‘¦ ∈ ran π‘”βˆ€π‘§ ∈ ran 𝑔(((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§)))
3534, 12, 6wral 3061 . . . . 5 wff βˆ€π‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran π‘”βˆ€π‘§ ∈ ran 𝑔(((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§)))
3616, 15wceq 1541 . . . . . . . 8 wff (π‘₯β„Žπ‘¦) = 𝑦
3715, 13, 9co 7408 . . . . . . . . 9 class (π‘¦β„Žπ‘₯)
3837, 15wceq 1541 . . . . . . . 8 wff (π‘¦β„Žπ‘₯) = 𝑦
3936, 38wa 396 . . . . . . 7 wff ((π‘₯β„Žπ‘¦) = 𝑦 ∧ (π‘¦β„Žπ‘₯) = 𝑦)
4039, 14, 6wral 3061 . . . . . 6 wff βˆ€π‘¦ ∈ ran 𝑔((π‘₯β„Žπ‘¦) = 𝑦 ∧ (π‘¦β„Žπ‘₯) = 𝑦)
4140, 12, 6wrex 3070 . . . . 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 5210 . 2 class {βŸ¨π‘”, β„ŽβŸ© ∣ ((𝑔 ∈ AbelOp ∧ β„Ž:(ran 𝑔 Γ— ran 𝑔)⟢ran 𝑔) ∧ (βˆ€π‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran π‘”βˆ€π‘§ ∈ ran 𝑔(((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§))) ∧ βˆƒπ‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran 𝑔((π‘₯β„Žπ‘¦) = 𝑦 ∧ (π‘¦β„Žπ‘₯) = 𝑦)))}
451, 44wceq 1541 1 wff RingOps = {βŸ¨π‘”, β„ŽβŸ© ∣ ((𝑔 ∈ AbelOp ∧ β„Ž:(ran 𝑔 Γ— ran 𝑔)⟢ran 𝑔) ∧ (βˆ€π‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran π‘”βˆ€π‘§ ∈ ran 𝑔(((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§))) ∧ βˆƒπ‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran 𝑔((π‘₯β„Žπ‘¦) = 𝑦 ∧ (π‘¦β„Žπ‘₯) = 𝑦)))}
Colors of variables: wff setvar class
This definition is referenced by:  relrngo  36759  isrngo  36760
  Copyright terms: Public domain W3C validator