Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rng0 Structured version   Visualization version   GIF version

Definition df-rng0 41660
Description: Define class of all (non-unital) rings. A non-unital ring (or rng, or pseudoring) is a set equipped with two everywhere-defined internal operations, whose first one is an additive abelian group operation and the second one is a multiplicative semigroup operation, and where the addition is left- and right-distributive for the multiplication. Definition of a pseudo-ring in section I.8.1 of [BourbakiAlg1] p. 93 or the definition of a ring in part Preliminaries of [Roman] p. 18. As almost always in mathematics, "non-unital" means "not necessarily unital". Therefore, by talking about a ring (in general) or a non-unital ring the "unital" case is always included. In contrast to a unital ring, the commutativity of addition must be postulated and cannot be proven from the other conditions. (Contributed by AV, 6-Jan-2020.)
Assertion
Ref Expression
df-rng0 Rng = {𝑓 ∈ Abel ∣ ((mulGrp‘𝑓) ∈ SGrp ∧ [(Base‘𝑓) / 𝑏][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
Distinct variable group:   𝑓,𝑏,𝑝,𝑡,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-rng0
StepHypRef Expression
1 crng 41659 . 2 class Rng
2 vf . . . . . . 7 setvar 𝑓
32cv 1473 . . . . . 6 class 𝑓
4 cmgp 18258 . . . . . 6 class mulGrp
53, 4cfv 5790 . . . . 5 class (mulGrp‘𝑓)
6 csgrp 17052 . . . . 5 class SGrp
75, 6wcel 1976 . . . 4 wff (mulGrp‘𝑓) ∈ SGrp
8 vx . . . . . . . . . . . . . 14 setvar 𝑥
98cv 1473 . . . . . . . . . . . . 13 class 𝑥
10 vy . . . . . . . . . . . . . . 15 setvar 𝑦
1110cv 1473 . . . . . . . . . . . . . 14 class 𝑦
12 vz . . . . . . . . . . . . . . 15 setvar 𝑧
1312cv 1473 . . . . . . . . . . . . . 14 class 𝑧
14 vp . . . . . . . . . . . . . . 15 setvar 𝑝
1514cv 1473 . . . . . . . . . . . . . 14 class 𝑝
1611, 13, 15co 6527 . . . . . . . . . . . . 13 class (𝑦𝑝𝑧)
17 vt . . . . . . . . . . . . . 14 setvar 𝑡
1817cv 1473 . . . . . . . . . . . . 13 class 𝑡
199, 16, 18co 6527 . . . . . . . . . . . 12 class (𝑥𝑡(𝑦𝑝𝑧))
209, 11, 18co 6527 . . . . . . . . . . . . 13 class (𝑥𝑡𝑦)
219, 13, 18co 6527 . . . . . . . . . . . . 13 class (𝑥𝑡𝑧)
2220, 21, 15co 6527 . . . . . . . . . . . 12 class ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
2319, 22wceq 1474 . . . . . . . . . . 11 wff (𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
249, 11, 15co 6527 . . . . . . . . . . . . 13 class (𝑥𝑝𝑦)
2524, 13, 18co 6527 . . . . . . . . . . . 12 class ((𝑥𝑝𝑦)𝑡𝑧)
2611, 13, 18co 6527 . . . . . . . . . . . . 13 class (𝑦𝑡𝑧)
2721, 26, 15co 6527 . . . . . . . . . . . 12 class ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
2825, 27wceq 1474 . . . . . . . . . . 11 wff ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
2923, 28wa 382 . . . . . . . . . 10 wff ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
30 vb . . . . . . . . . . 11 setvar 𝑏
3130cv 1473 . . . . . . . . . 10 class 𝑏
3229, 12, 31wral 2895 . . . . . . . . 9 wff 𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
3332, 10, 31wral 2895 . . . . . . . 8 wff 𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
3433, 8, 31wral 2895 . . . . . . 7 wff 𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
35 cmulr 15715 . . . . . . . 8 class .r
363, 35cfv 5790 . . . . . . 7 class (.r𝑓)
3734, 17, 36wsbc 3401 . . . . . 6 wff [(.r𝑓) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
38 cplusg 15714 . . . . . . 7 class +g
393, 38cfv 5790 . . . . . 6 class (+g𝑓)
4037, 14, 39wsbc 3401 . . . . 5 wff [(+g𝑓) / 𝑝][(.r𝑓) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
41 cbs 15641 . . . . . 6 class Base
423, 41cfv 5790 . . . . 5 class (Base‘𝑓)
4340, 30, 42wsbc 3401 . . . 4 wff [(Base‘𝑓) / 𝑏][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
447, 43wa 382 . . 3 wff ((mulGrp‘𝑓) ∈ SGrp ∧ [(Base‘𝑓) / 𝑏][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))
45 cabl 17963 . . 3 class Abel
4644, 2, 45crab 2899 . 2 class {𝑓 ∈ Abel ∣ ((mulGrp‘𝑓) ∈ SGrp ∧ [(Base‘𝑓) / 𝑏][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
471, 46wceq 1474 1 wff Rng = {𝑓 ∈ Abel ∣ ((mulGrp‘𝑓) ∈ SGrp ∧ [(Base‘𝑓) / 𝑏][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
Colors of variables: wff setvar class
This definition is referenced by:  isrng  41661
  Copyright terms: Public domain W3C validator