Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rng Structured version   Unicode version

Definition df-rng 16997
 Description: Define class of all (unital) rings. A unital ring is a set equipped with two everywhere-defined internal operations, whose first one is an additive group structure and the second one is a multiplicative monoid structure, and where the addition is left- and right-distributive for the multiplication. Definition of a ring in [BourbakiAlg1] p. 92 or of a ring with identity in [Roman] p. 19. So that the additive structure must be abelian (see rngcom 17023), care must be taken that in the case of a non-unital ring, the commutativity of addition must be postulated and cannot be proved from the other conditions. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 27-Dec-2014.)
Assertion
Ref Expression
df-rng mulGrp
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-rng
StepHypRef Expression
1 crg 16995 . 2
2 vf . . . . . . 7
32cv 1378 . . . . . 6
4 cmgp 16940 . . . . . 6 mulGrp
53, 4cfv 5587 . . . . 5 mulGrp
6 cmnd 15725 . . . . 5
75, 6wcel 1767 . . . 4 mulGrp
8 vx . . . . . . . . . . . . . 14
98cv 1378 . . . . . . . . . . . . 13
10 vy . . . . . . . . . . . . . . 15
1110cv 1378 . . . . . . . . . . . . . 14
12 vz . . . . . . . . . . . . . . 15
1312cv 1378 . . . . . . . . . . . . . 14
14 vp . . . . . . . . . . . . . . 15
1514cv 1378 . . . . . . . . . . . . . 14
1611, 13, 15co 6283 . . . . . . . . . . . . 13
17 vt . . . . . . . . . . . . . 14
1817cv 1378 . . . . . . . . . . . . 13
199, 16, 18co 6283 . . . . . . . . . . . 12
209, 11, 18co 6283 . . . . . . . . . . . . 13
219, 13, 18co 6283 . . . . . . . . . . . . 13
2220, 21, 15co 6283 . . . . . . . . . . . 12
2319, 22wceq 1379 . . . . . . . . . . 11
249, 11, 15co 6283 . . . . . . . . . . . . 13
2524, 13, 18co 6283 . . . . . . . . . . . 12
2611, 13, 18co 6283 . . . . . . . . . . . . 13
2721, 26, 15co 6283 . . . . . . . . . . . 12
2825, 27wceq 1379 . . . . . . . . . . 11
2923, 28wa 369 . . . . . . . . . 10
30 vr . . . . . . . . . . 11
3130cv 1378 . . . . . . . . . 10
3229, 12, 31wral 2814 . . . . . . . . 9
3332, 10, 31wral 2814 . . . . . . . 8
3433, 8, 31wral 2814 . . . . . . 7
35 cmulr 14555 . . . . . . . 8
363, 35cfv 5587 . . . . . . 7
3734, 17, 36wsbc 3331 . . . . . 6
38 cplusg 14554 . . . . . . 7
393, 38cfv 5587 . . . . . 6
4037, 14, 39wsbc 3331 . . . . 5
41 cbs 14489 . . . . . 6
423, 41cfv 5587 . . . . 5
4340, 30, 42wsbc 3331 . . . 4
447, 43wa 369 . . 3 mulGrp
45 cgrp 15726 . . 3
4644, 2, 45crab 2818 . 2 mulGrp
471, 46wceq 1379 1 mulGrp
 Colors of variables: wff setvar class This definition is referenced by:  isrng  16999
 Copyright terms: Public domain W3C validator