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

Definition df-rng0 39147
 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 mulGrp SGrp
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-rng0
StepHypRef Expression
1 crng 39146 . 2 Rng
2 vf . . . . . . 7
32cv 1436 . . . . . 6
4 cmgp 17711 . . . . . 6 mulGrp
53, 4cfv 5598 . . . . 5 mulGrp
6 csgrp 16514 . . . . 5 SGrp
75, 6wcel 1868 . . . 4 mulGrp SGrp
8 vx . . . . . . . . . . . . . 14
98cv 1436 . . . . . . . . . . . . 13
10 vy . . . . . . . . . . . . . . 15
1110cv 1436 . . . . . . . . . . . . . 14
12 vz . . . . . . . . . . . . . . 15
1312cv 1436 . . . . . . . . . . . . . 14
14 vp . . . . . . . . . . . . . . 15
1514cv 1436 . . . . . . . . . . . . . 14
1611, 13, 15co 6302 . . . . . . . . . . . . 13
17 vt . . . . . . . . . . . . . 14
1817cv 1436 . . . . . . . . . . . . 13
199, 16, 18co 6302 . . . . . . . . . . . 12
209, 11, 18co 6302 . . . . . . . . . . . . 13
219, 13, 18co 6302 . . . . . . . . . . . . 13
2220, 21, 15co 6302 . . . . . . . . . . . 12
2319, 22wceq 1437 . . . . . . . . . . 11
249, 11, 15co 6302 . . . . . . . . . . . . 13
2524, 13, 18co 6302 . . . . . . . . . . . 12
2611, 13, 18co 6302 . . . . . . . . . . . . 13
2721, 26, 15co 6302 . . . . . . . . . . . 12
2825, 27wceq 1437 . . . . . . . . . . 11
2923, 28wa 370 . . . . . . . . . 10
30 vb . . . . . . . . . . 11
3130cv 1436 . . . . . . . . . 10
3229, 12, 31wral 2775 . . . . . . . . 9
3332, 10, 31wral 2775 . . . . . . . 8
3433, 8, 31wral 2775 . . . . . . 7
35 cmulr 15179 . . . . . . . 8
363, 35cfv 5598 . . . . . . 7
3734, 17, 36wsbc 3299 . . . . . 6
38 cplusg 15178 . . . . . . 7
393, 38cfv 5598 . . . . . 6
4037, 14, 39wsbc 3299 . . . . 5
41 cbs 15109 . . . . . 6
423, 41cfv 5598 . . . . 5
4340, 30, 42wsbc 3299 . . . 4
447, 43wa 370 . . 3 mulGrp SGrp
45 cabl 17419 . . 3
4644, 2, 45crab 2779 . 2 mulGrp SGrp
471, 46wceq 1437 1 Rng mulGrp SGrp
 Colors of variables: wff setvar class This definition is referenced by:  isrng  39148
 Copyright terms: Public domain W3C validator