Definition df-ring 13134

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 13167), 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-ring	|- Ring = { f e. Grp | ( (mulGrp ` f ) e. Mnd /\ [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. A. x e. r A. y e. r A. z e. 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 ) ) ) ) }

Distinct variable group:   f, p, r, t, x, y, z

Detailed syntax breakdown of Definition df-ring

Step	Hyp	Ref	Expression
1		crg 13132	. 2 class Ring
2		vf	. . . . . . 7 setvar f
3	2	cv 1352	. . . . . 6 class f
4		cmgp 13083	. . . . . 6 class mulGrp
5	3, 4	cfv 5216	. . . . 5 class (mulGrp ` f )
6		cmnd 12771	. . . . 5 class Mnd
7	5, 6	wcel 2148	. . . 4 wff (mulGrp ` f ) e. Mnd
8		vx	. . . . . . . . . . . . . 14 setvar x
9	8	cv 1352	. . . . . . . . . . . . 13 class x
10		vy	. . . . . . . . . . . . . . 15 setvar y
11	10	cv 1352	. . . . . . . . . . . . . 14 class y
12		vz	. . . . . . . . . . . . . . 15 setvar z
13	12	cv 1352	. . . . . . . . . . . . . 14 class z
14		vp	. . . . . . . . . . . . . . 15 setvar p
15	14	cv 1352	. . . . . . . . . . . . . 14 class p
16	11, 13, 15	co 5874	. . . . . . . . . . . . 13 class ( y p z )
17		vt	. . . . . . . . . . . . . 14 setvar t
18	17	cv 1352	. . . . . . . . . . . . 13 class t
19	9, 16, 18	co 5874	. . . . . . . . . . . 12 class ( x t ( y p z ) )
20	9, 11, 18	co 5874	. . . . . . . . . . . . 13 class ( x t y )
21	9, 13, 18	co 5874	. . . . . . . . . . . . 13 class ( x t z )
22	20, 21, 15	co 5874	. . . . . . . . . . . 12 class ( ( x t y ) p ( x t z ) )
23	19, 22	wceq 1353	. . . . . . . . . . 11 wff ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) )
24	9, 11, 15	co 5874	. . . . . . . . . . . . 13 class ( x p y )
25	24, 13, 18	co 5874	. . . . . . . . . . . 12 class ( ( x p y ) t z )
26	11, 13, 18	co 5874	. . . . . . . . . . . . 13 class ( y t z )
27	21, 26, 15	co 5874	. . . . . . . . . . . 12 class ( ( x t z ) p ( y t z ) )
28	25, 27	wceq 1353	. . . . . . . . . . 11 wff ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) )
29	23, 28	wa 104	. . . . . . . . . 10 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 ) ) )
30		vr	. . . . . . . . . . 11 setvar r
31	30	cv 1352	. . . . . . . . . 10 class r
32	29, 12, 31	wral 2455	. . . . . . . . 9 wff A. z e. 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 ) ) )
33	32, 10, 31	wral 2455	. . . . . . . 8 wff A. y e. r A. z e. 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 ) ) )
34	33, 8, 31	wral 2455	. . . . . . 7 wff A. x e. r A. y e. r A. z e. 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 ) ) )
35		cmulr 12531	. . . . . . . 8 class .r
36	3, 35	cfv 5216	. . . . . . 7 class ( .r ` f )
37	34, 17, 36	wsbc 2962	. . . . . 6 wff [. ( .r ` f ) / t ]. A. x e. r A. y e. r A. z e. 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 ) ) )
38		cplusg 12530	. . . . . . 7 class +g
39	3, 38	cfv 5216	. . . . . 6 class ( +g ` f )
40	37, 14, 39	wsbc 2962	. . . . 5 wff [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. A. x e. r A. y e. r A. z e. 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		cbs 12456	. . . . . 6 class Base
42	3, 41	cfv 5216	. . . . 5 class ( Base ` f )
43	40, 30, 42	wsbc 2962	. . . 4 wff [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. A. x e. r A. y e. r A. z e. 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 104	. . 3 wff ( (mulGrp ` f ) e. Mnd /\ [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. A. x e. r A. y e. r A. z e. 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		cgrp 12831	. . 3 class Grp
46	44, 2, 45	crab 2459	. 2 class { f e. Grp | ( (mulGrp ` f ) e. Mnd /\ [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. A. x e. r A. y e. r A. z e. 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 ) ) ) ) }
47	1, 46	wceq 1353	1 wff Ring = { f e. Grp | ( (mulGrp ` f ) e. Mnd /\ [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. A. x e. r A. y e. r A. z e. 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 ) ) ) ) }

This definition is referenced by:  isring  13136