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

Definition df-rng 15668
 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. So that the additive structure must be abelian (see rngcom 15697), 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 15665 . 2
2 vf . . . . . . 7
32cv 1652 . . . . . 6
4 cmgp 15653 . . . . . 6 mulGrp
53, 4cfv 5457 . . . . 5 mulGrp
6 cmnd 14689 . . . . 5
75, 6wcel 1726 . . . 4 mulGrp
8 vx . . . . . . . . . . . . . 14
98cv 1652 . . . . . . . . . . . . 13
10 vy . . . . . . . . . . . . . . 15
1110cv 1652 . . . . . . . . . . . . . 14
12 vz . . . . . . . . . . . . . . 15
1312cv 1652 . . . . . . . . . . . . . 14
14 vp . . . . . . . . . . . . . . 15
1514cv 1652 . . . . . . . . . . . . . 14
1611, 13, 15co 6084 . . . . . . . . . . . . 13
17 vt . . . . . . . . . . . . . 14
1817cv 1652 . . . . . . . . . . . . 13
199, 16, 18co 6084 . . . . . . . . . . . 12
209, 11, 18co 6084 . . . . . . . . . . . . 13
219, 13, 18co 6084 . . . . . . . . . . . . 13
2220, 21, 15co 6084 . . . . . . . . . . . 12
2319, 22wceq 1653 . . . . . . . . . . 11
249, 11, 15co 6084 . . . . . . . . . . . . 13
2524, 13, 18co 6084 . . . . . . . . . . . 12
2611, 13, 18co 6084 . . . . . . . . . . . . 13
2721, 26, 15co 6084 . . . . . . . . . . . 12
2825, 27wceq 1653 . . . . . . . . . . 11
2923, 28wa 360 . . . . . . . . . 10
30 vr . . . . . . . . . . 11
3130cv 1652 . . . . . . . . . 10
3229, 12, 31wral 2707 . . . . . . . . 9
3332, 10, 31wral 2707 . . . . . . . 8
3433, 8, 31wral 2707 . . . . . . 7
35 cmulr 13535 . . . . . . . 8
363, 35cfv 5457 . . . . . . 7
3734, 17, 36wsbc 3163 . . . . . 6
38 cplusg 13534 . . . . . . 7
393, 38cfv 5457 . . . . . 6
4037, 14, 39wsbc 3163 . . . . 5
41 cbs 13474 . . . . . 6
423, 41cfv 5457 . . . . 5
4340, 30, 42wsbc 3163 . . . 4
447, 43wa 360 . . 3 mulGrp
45 cgrp 14690 . . 3
4644, 2, 45crab 2711 . 2 mulGrp
471, 46wceq 1653 1 mulGrp
 Colors of variables: wff set class This definition is referenced by:  isrng  15673
 Copyright terms: Public domain W3C validator