Definition df-rng0 45321

Description: Define class of all (non-unital) rings. A non-unital ring (or rng, or pseudoring) is a set equipped with two everywhere-defined internal operations, whose first one is an additive abelian group operation and the second one is a multiplicative semigroup operation, and where the addition is left- and right-distributive for the multiplication. Definition of a pseudo-ring in section I.8.1 of [BourbakiAlg1] p. 93 or the definition of a ring in part Preliminaries of [Roman] p. 18. As almost always in mathematics, "non-unital" means "not necessarily unital". Therefore, by talking about a ring (in general) or a non-unital ring the "unital" case is always included. In contrast to a unital ring, the commutativity of addition must be postulated and cannot be proven from the other conditions. (Contributed by AV, 6-Jan-2020.)

Assertion

Ref	Expression
df-rng0	⊢ Rng = {𝑓 ∈ Abel ∣ ((mulGrp‘𝑓) ∈ Smgrp ∧ [(Base‘𝑓) / 𝑏][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}

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

Detailed syntax breakdown of Definition df-rng0

Step	Hyp	Ref	Expression
1		crng 45320	. 2 class Rng
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1538	. . . . . 6 class 𝑓
4		cmgp 19635	. . . . . 6 class mulGrp
5	3, 4	cfv 6418	. . . . 5 class (mulGrp‘𝑓)
6		csgrp 18289	. . . . 5 class Smgrp
7	5, 6	wcel 2108	. . . 4 wff (mulGrp‘𝑓) ∈ Smgrp
8		vx	. . . . . . . . . . . . . 14 setvar 𝑥
9	8	cv 1538	. . . . . . . . . . . . 13 class 𝑥
10		vy	. . . . . . . . . . . . . . 15 setvar 𝑦
11	10	cv 1538	. . . . . . . . . . . . . 14 class 𝑦
12		vz	. . . . . . . . . . . . . . 15 setvar 𝑧
13	12	cv 1538	. . . . . . . . . . . . . 14 class 𝑧
14		vp	. . . . . . . . . . . . . . 15 setvar 𝑝
15	14	cv 1538	. . . . . . . . . . . . . 14 class 𝑝
16	11, 13, 15	co 7255	. . . . . . . . . . . . 13 class (𝑦𝑝𝑧)
17		vt	. . . . . . . . . . . . . 14 setvar 𝑡
18	17	cv 1538	. . . . . . . . . . . . 13 class 𝑡
19	9, 16, 18	co 7255	. . . . . . . . . . . 12 class (𝑥𝑡(𝑦𝑝𝑧))
20	9, 11, 18	co 7255	. . . . . . . . . . . . 13 class (𝑥𝑡𝑦)
21	9, 13, 18	co 7255	. . . . . . . . . . . . 13 class (𝑥𝑡𝑧)
22	20, 21, 15	co 7255	. . . . . . . . . . . 12 class ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
23	19, 22	wceq 1539	. . . . . . . . . . 11 wff (𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
24	9, 11, 15	co 7255	. . . . . . . . . . . . 13 class (𝑥𝑝𝑦)
25	24, 13, 18	co 7255	. . . . . . . . . . . 12 class ((𝑥𝑝𝑦)𝑡𝑧)
26	11, 13, 18	co 7255	. . . . . . . . . . . . 13 class (𝑦𝑡𝑧)
27	21, 26, 15	co 7255	. . . . . . . . . . . 12 class ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
28	25, 27	wceq 1539	. . . . . . . . . . 11 wff ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
29	23, 28	wa 395	. . . . . . . . . 10 wff ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
30		vb	. . . . . . . . . . 11 setvar 𝑏
31	30	cv 1538	. . . . . . . . . 10 class 𝑏
32	29, 12, 31	wral 3063	. . . . . . . . 9 wff ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
33	32, 10, 31	wral 3063	. . . . . . . 8 wff ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
34	33, 8, 31	wral 3063	. . . . . . 7 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
35		cmulr 16889	. . . . . . . 8 class .r
36	3, 35	cfv 6418	. . . . . . 7 class (.r‘𝑓)
37	34, 17, 36	wsbc 3711	. . . . . 6 wff [(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
38		cplusg 16888	. . . . . . 7 class +g
39	3, 38	cfv 6418	. . . . . 6 class (+g‘𝑓)
40	37, 14, 39	wsbc 3711	. . . . 5 wff [(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
41		cbs 16840	. . . . . 6 class Base
42	3, 41	cfv 6418	. . . . 5 class (Base‘𝑓)
43	40, 30, 42	wsbc 3711	. . . 4 wff [(Base‘𝑓) / 𝑏][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
44	7, 43	wa 395	. . 3 wff ((mulGrp‘𝑓) ∈ Smgrp ∧ [(Base‘𝑓) / 𝑏][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))
45		cabl 19302	. . 3 class Abel
46	44, 2, 45	crab 3067	. 2 class {𝑓 ∈ Abel ∣ ((mulGrp‘𝑓) ∈ Smgrp ∧ [(Base‘𝑓) / 𝑏][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
47	1, 46	wceq 1539	1 wff Rng = {𝑓 ∈ Abel ∣ ((mulGrp‘𝑓) ∈ Smgrp ∧ [(Base‘𝑓) / 𝑏][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}

This definition is referenced by:  isrng  45322