# Metamath Proof Explorer

## Definition df-ring

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 1 in BourbakiAlg1 p. 92 or definition of a ring with identity in part Preliminaries of Roman p. 19. So that the additive structure must be abelian (see ringcom ), 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)

Ref Expression
Assertion df-ring

### Detailed syntax breakdown

Step Hyp Ref Expression
0 crg ${class}\mathrm{Ring}$
1 vf ${setvar}{f}$
2 cgrp ${class}\mathrm{Grp}$
3 cmgp ${class}\mathrm{mulGrp}$
4 1 cv ${setvar}{f}$
5 4 3 cfv ${class}{\mathrm{mulGrp}}_{{f}}$
6 cmnd ${class}\mathrm{Mnd}$
7 5 6 wcel ${wff}{\mathrm{mulGrp}}_{{f}}\in \mathrm{Mnd}$
8 cbs ${class}\mathrm{Base}$
9 4 8 cfv ${class}{\mathrm{Base}}_{{f}}$
10 vr ${setvar}{r}$
11 cplusg ${class}{+}_{𝑔}$
12 4 11 cfv ${class}{+}_{{f}}$
13 vp ${setvar}{p}$
14 cmulr ${class}{\cdot }_{𝑟}$
15 4 14 cfv ${class}{\cdot }_{{f}}$
16 vt ${setvar}{t}$
17 vx ${setvar}{x}$
18 10 cv ${setvar}{r}$
19 vy ${setvar}{y}$
20 vz ${setvar}{z}$
21 17 cv ${setvar}{x}$
22 16 cv ${setvar}{t}$
23 19 cv ${setvar}{y}$
24 13 cv ${setvar}{p}$
25 20 cv ${setvar}{z}$
26 23 25 24 co ${class}\left({y}{p}{z}\right)$
27 21 26 22 co ${class}\left({x}{t}\left({y}{p}{z}\right)\right)$
28 21 23 22 co ${class}\left({x}{t}{y}\right)$
29 21 25 22 co ${class}\left({x}{t}{z}\right)$
30 28 29 24 co ${class}\left(\left({x}{t}{y}\right){p}\left({x}{t}{z}\right)\right)$
31 27 30 wceq ${wff}{x}{t}\left({y}{p}{z}\right)=\left({x}{t}{y}\right){p}\left({x}{t}{z}\right)$
32 21 23 24 co ${class}\left({x}{p}{y}\right)$
33 32 25 22 co ${class}\left(\left({x}{p}{y}\right){t}{z}\right)$
34 23 25 22 co ${class}\left({y}{t}{z}\right)$
35 29 34 24 co ${class}\left(\left({x}{t}{z}\right){p}\left({y}{t}{z}\right)\right)$
36 33 35 wceq ${wff}\left({x}{p}{y}\right){t}{z}=\left({x}{t}{z}\right){p}\left({y}{t}{z}\right)$
37 31 36 wa ${wff}\left({x}{t}\left({y}{p}{z}\right)=\left({x}{t}{y}\right){p}\left({x}{t}{z}\right)\wedge \left({x}{p}{y}\right){t}{z}=\left({x}{t}{z}\right){p}\left({y}{t}{z}\right)\right)$
38 37 20 18 wral ${wff}\forall {z}\in {r}\phantom{\rule{.4em}{0ex}}\left({x}{t}\left({y}{p}{z}\right)=\left({x}{t}{y}\right){p}\left({x}{t}{z}\right)\wedge \left({x}{p}{y}\right){t}{z}=\left({x}{t}{z}\right){p}\left({y}{t}{z}\right)\right)$
39 38 19 18 wral ${wff}\forall {y}\in {r}\phantom{\rule{.4em}{0ex}}\forall {z}\in {r}\phantom{\rule{.4em}{0ex}}\left({x}{t}\left({y}{p}{z}\right)=\left({x}{t}{y}\right){p}\left({x}{t}{z}\right)\wedge \left({x}{p}{y}\right){t}{z}=\left({x}{t}{z}\right){p}\left({y}{t}{z}\right)\right)$
40 39 17 18 wral ${wff}\forall {x}\in {r}\phantom{\rule{.4em}{0ex}}\forall {y}\in {r}\phantom{\rule{.4em}{0ex}}\forall {z}\in {r}\phantom{\rule{.4em}{0ex}}\left({x}{t}\left({y}{p}{z}\right)=\left({x}{t}{y}\right){p}\left({x}{t}{z}\right)\wedge \left({x}{p}{y}\right){t}{z}=\left({x}{t}{z}\right){p}\left({y}{t}{z}\right)\right)$
41 40 16 15 wsbc
42 41 13 12 wsbc
43 42 10 9 wsbc
44 7 43 wa
45 44 1 2 crab
46 0 45 wceq