Definition df-srg 20326

Description: Define class of all semirings. A semiring is a set equipped with two everywhere-defined internal operations, whose first one is an additive commutative monoid structure and the second one is a multiplicative monoid structure, and where multiplication is (left- and right-) distributive over addition. Like with rings (df-ring 20374), the additive identity is an absorbing element of the multiplicative law, but in the case of semirings, this has to be part of the definition, as it cannot be deduced from distributivity alone. Definition of [Golan] p. 1. Note that our semirings are unital. Such semirings are sometimes called "rigs", being "rings without negatives". (Contributed by Thierry Arnoux, 21-Mar-2018.)

Assertion

Ref	Expression
df-srg	⊢ SRing = {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}

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

Detailed syntax breakdown of Definition df-srg

Step	Hyp	Ref	Expression
1		csrg 20325	. 2 class SRing
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1569	. . . . . 6 class 𝑓
4		cmgp 20273	. . . . . 6 class mulGrp
5	3, 4	cfv 6533	. . . . 5 class (mulGrp‘𝑓)
6		cmnd 18836	. . . . 5 class Mnd
7	5, 6	wcel 2145	. . . 4 wff (mulGrp‘𝑓) ∈ Mnd
8		vx	. . . . . . . . . . . . . . . 16 setvar 𝑥
9	8	cv 1569	. . . . . . . . . . . . . . 15 class 𝑥
10		vy	. . . . . . . . . . . . . . . . 17 setvar 𝑦
11	10	cv 1569	. . . . . . . . . . . . . . . 16 class 𝑦
12		vz	. . . . . . . . . . . . . . . . 17 setvar 𝑧
13	12	cv 1569	. . . . . . . . . . . . . . . 16 class 𝑧
14		vp	. . . . . . . . . . . . . . . . 17 setvar 𝑝
15	14	cv 1569	. . . . . . . . . . . . . . . 16 class 𝑝
16	11, 13, 15	co 7413	. . . . . . . . . . . . . . 15 class (𝑦𝑝𝑧)
17		vt	. . . . . . . . . . . . . . . 16 setvar 𝑡
18	17	cv 1569	. . . . . . . . . . . . . . 15 class 𝑡
19	9, 16, 18	co 7413	. . . . . . . . . . . . . 14 class (𝑥𝑡(𝑦𝑝𝑧))
20	9, 11, 18	co 7413	. . . . . . . . . . . . . . 15 class (𝑥𝑡𝑦)
21	9, 13, 18	co 7413	. . . . . . . . . . . . . . 15 class (𝑥𝑡𝑧)
22	20, 21, 15	co 7413	. . . . . . . . . . . . . 14 class ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
23	19, 22	wceq 1570	. . . . . . . . . . . . 13 wff (𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
24	9, 11, 15	co 7413	. . . . . . . . . . . . . . 15 class (𝑥𝑝𝑦)
25	24, 13, 18	co 7413	. . . . . . . . . . . . . 14 class ((𝑥𝑝𝑦)𝑡𝑧)
26	11, 13, 18	co 7413	. . . . . . . . . . . . . . 15 class (𝑦𝑡𝑧)
27	21, 26, 15	co 7413	. . . . . . . . . . . . . 14 class ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
28	25, 27	wceq 1570	. . . . . . . . . . . . 13 wff ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
29	23, 28	wa 401	. . . . . . . . . . . 12 wff ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
30		vr	. . . . . . . . . . . . 13 setvar 𝑟
31	30	cv 1569	. . . . . . . . . . . 12 class 𝑟
32	29, 12, 31	wral 3076	. . . . . . . . . . 11 wff ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
33	32, 10, 31	wral 3076	. . . . . . . . . 10 wff ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
34		vn	. . . . . . . . . . . . . 14 setvar 𝑛
35	34	cv 1569	. . . . . . . . . . . . 13 class 𝑛
36	35, 9, 18	co 7413	. . . . . . . . . . . 12 class (𝑛𝑡𝑥)
37	36, 35	wceq 1570	. . . . . . . . . . 11 wff (𝑛𝑡𝑥) = 𝑛
38	9, 35, 18	co 7413	. . . . . . . . . . . 12 class (𝑥𝑡𝑛)
39	38, 35	wceq 1570	. . . . . . . . . . 11 wff (𝑥𝑡𝑛) = 𝑛
40	37, 39	wa 401	. . . . . . . . . 10 wff ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)
41	33, 40	wa 401	. . . . . . . . 9 wff (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
42	41, 8, 31	wral 3076	. . . . . . . 8 wff ∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
43		c0g 17524	. . . . . . . . 9 class 0g
44	3, 43	cfv 6533	. . . . . . . 8 class (0g‘𝑓)
45	42, 34, 44	wsbc 3739	. . . . . . 7 wff [(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
46		cmulr 17343	. . . . . . . 8 class .r
47	3, 46	cfv 6533	. . . . . . 7 class (.r‘𝑓)
48	45, 17, 47	wsbc 3739	. . . . . 6 wff [(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
49		cplusg 17342	. . . . . . 7 class +g
50	3, 49	cfv 6533	. . . . . 6 class (+g‘𝑓)
51	48, 14, 50	wsbc 3739	. . . . 5 wff [(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
52		cbs 17301	. . . . . 6 class Base
53	3, 52	cfv 6533	. . . . 5 class (Base‘𝑓)
54	51, 30, 53	wsbc 3739	. . . 4 wff [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
55	7, 54	wa 401	. . 3 wff ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))
56		ccmn 19907	. . 3 class CMnd
57	55, 2, 56	crab 3412	. 2 class {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
58	1, 57	wceq 1570	1 wff SRing = {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}

This definition is used by:  issrg  20327