Definition df-ring 13956

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 13989), 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 = {𝑓 ∈ Grp ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}

Distinct variable group:   𝑓,𝑝,𝑟,𝑡,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ring

Step	Hyp	Ref	Expression
1		crg 13954	. 2 class Ring
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1394	. . . . . 6 class 𝑓
4		cmgp 13878	. . . . . 6 class mulGrp
5	3, 4	cfv 5317	. . . . 5 class (mulGrp‘𝑓)
6		cmnd 13444	. . . . 5 class Mnd
7	5, 6	wcel 2200	. . . 4 wff (mulGrp‘𝑓) ∈ Mnd
8		vx	. . . . . . . . . . . . . 14 setvar 𝑥
9	8	cv 1394	. . . . . . . . . . . . 13 class 𝑥
10		vy	. . . . . . . . . . . . . . 15 setvar 𝑦
11	10	cv 1394	. . . . . . . . . . . . . 14 class 𝑦
12		vz	. . . . . . . . . . . . . . 15 setvar 𝑧
13	12	cv 1394	. . . . . . . . . . . . . 14 class 𝑧
14		vp	. . . . . . . . . . . . . . 15 setvar 𝑝
15	14	cv 1394	. . . . . . . . . . . . . 14 class 𝑝
16	11, 13, 15	co 6000	. . . . . . . . . . . . 13 class (𝑦𝑝𝑧)
17		vt	. . . . . . . . . . . . . 14 setvar 𝑡
18	17	cv 1394	. . . . . . . . . . . . 13 class 𝑡
19	9, 16, 18	co 6000	. . . . . . . . . . . 12 class (𝑥𝑡(𝑦𝑝𝑧))
20	9, 11, 18	co 6000	. . . . . . . . . . . . 13 class (𝑥𝑡𝑦)
21	9, 13, 18	co 6000	. . . . . . . . . . . . 13 class (𝑥𝑡𝑧)
22	20, 21, 15	co 6000	. . . . . . . . . . . 12 class ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
23	19, 22	wceq 1395	. . . . . . . . . . 11 wff (𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
24	9, 11, 15	co 6000	. . . . . . . . . . . . 13 class (𝑥𝑝𝑦)
25	24, 13, 18	co 6000	. . . . . . . . . . . 12 class ((𝑥𝑝𝑦)𝑡𝑧)
26	11, 13, 18	co 6000	. . . . . . . . . . . . 13 class (𝑦𝑡𝑧)
27	21, 26, 15	co 6000	. . . . . . . . . . . 12 class ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
28	25, 27	wceq 1395	. . . . . . . . . . 11 wff ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
29	23, 28	wa 104	. . . . . . . . . 10 wff ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
30		vr	. . . . . . . . . . 11 setvar 𝑟
31	30	cv 1394	. . . . . . . . . 10 class 𝑟
32	29, 12, 31	wral 2508	. . . . . . . . 9 wff ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
33	32, 10, 31	wral 2508	. . . . . . . 8 wff ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
34	33, 8, 31	wral 2508	. . . . . . 7 wff ∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
35		cmulr 13106	. . . . . . . 8 class .r
36	3, 35	cfv 5317	. . . . . . 7 class (.r‘𝑓)
37	34, 17, 36	wsbc 3028	. . . . . 6 wff [(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
38		cplusg 13105	. . . . . . 7 class +g
39	3, 38	cfv 5317	. . . . . 6 class (+g‘𝑓)
40	37, 14, 39	wsbc 3028	. . . . 5 wff [(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
41		cbs 13027	. . . . . 6 class Base
42	3, 41	cfv 5317	. . . . 5 class (Base‘𝑓)
43	40, 30, 42	wsbc 3028	. . . 4 wff [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
44	7, 43	wa 104	. . 3 wff ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))
45		cgrp 13528	. . 3 class Grp
46	44, 2, 45	crab 2512	. 2 class {𝑓 ∈ Grp ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
47	1, 46	wceq 1395	1 wff Ring = {𝑓 ∈ Grp ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}

This definition is referenced by:  isring  13958