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 ⊢ Ring = f ∈ Grp | mulGrp f ∈ Mnd ∧ [˙Base f / r]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z

Detailed syntax breakdown

Step Hyp Ref Expression
0 crg class Ring
1 vf setvar f
2 cgrp class Grp
3 cmgp class mulGrp
4 1 cv setvar f
5 4 3 cfv class mulGrp f
6 cmnd class Mnd
7 5 6 wcel wff mulGrp f ∈ Mnd
8 cbs class Base
9 4 8 cfv class Base f
10 vr setvar r
11 cplusg class + 𝑔
12 4 11 cfv class + f
13 vp setvar p
14 cmulr class ⋅ 𝑟
15 4 14 cfv class ⋅ 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 y p z
27 21 26 22 co class x t y p z
28 21 23 22 co class x t y
29 21 25 22 co class x t z
30 28 29 24 co class x t y p x t z
31 27 30 wceq wff x t y p z = x t y p x t z
32 21 23 24 co class x p y
33 32 25 22 co class x p y t z
34 23 25 22 co class y t z
35 29 34 24 co class x t z p y t z
36 33 35 wceq wff x p y t z = x t z p y t z
37 31 36 wa wff x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
38 37 20 18 wral wff ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
39 38 19 18 wral wff ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
40 39 17 18 wral wff ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
41 40 16 15 wsbc wff [˙⋅ f / t]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
42 41 13 12 wsbc wff [˙+ f / p]˙ [˙⋅ f / t]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
43 42 10 9 wsbc wff [˙Base f / r]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
44 7 43 wa wff mulGrp f ∈ Mnd ∧ [˙Base f / r]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
45 44 1 2 crab class f ∈ Grp | mulGrp f ∈ Mnd ∧ [˙Base f / r]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
46 0 45 wceq wff Ring = f ∈ Grp | mulGrp f ∈ Mnd ∧ [˙Base f / r]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z