Definition df-srg 20464

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 20512), 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 20463	. 2 class SRing
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1569	. . . . . 6 class 𝑓
4		cmgp 20411	. . . . . 6 class mulGrp
5	3, 4	cfv 6566	. . . . 5 class (mulGrp‘𝑓)
6		cmnd 18973	. . . . 5 class Mnd
7	5, 6	wcel 2147	. . . 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 7451	. . . . . . . . . . . . . . 15 class (𝑦𝑝𝑧)
17		vt	. . . . . . . . . . . . . . . 16 setvar 𝑡
18	17	cv 1569	. . . . . . . . . . . . . . 15 class 𝑡
19	9, 16, 18	co 7451	. . . . . . . . . . . . . 14 class (𝑥𝑡(𝑦𝑝𝑧))
20	9, 11, 18	co 7451	. . . . . . . . . . . . . . 15 class (𝑥𝑡𝑦)
21	9, 13, 18	co 7451	. . . . . . . . . . . . . . 15 class (𝑥𝑡𝑧)
22	20, 21, 15	co 7451	. . . . . . . . . . . . . 14 class ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
23	19, 22	wceq 1570	. . . . . . . . . . . . 13 wff (𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
24	9, 11, 15	co 7451	. . . . . . . . . . . . . . 15 class (𝑥𝑝𝑦)
25	24, 13, 18	co 7451	. . . . . . . . . . . . . 14 class ((𝑥𝑝𝑦)𝑡𝑧)
26	11, 13, 18	co 7451	. . . . . . . . . . . . . . 15 class (𝑦𝑡𝑧)
27	21, 26, 15	co 7451	. . . . . . . . . . . . . 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 3080	. . . . . . . . . . 11 wff ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
33	32, 10, 31	wral 3080	. . . . . . . . . 10 wff ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
34		vn	. . . . . . . . . . . . . 14 setvar 𝑛
35	34	cv 1569	. . . . . . . . . . . . 13 class 𝑛
36	35, 9, 18	co 7451	. . . . . . . . . . . 12 class (𝑛𝑡𝑥)
37	36, 35	wceq 1570	. . . . . . . . . . 11 wff (𝑛𝑡𝑥) = 𝑛
38	9, 35, 18	co 7451	. . . . . . . . . . . 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 3080	. . . . . . . 8 wff ∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
43		c0g 17660	. . . . . . . . 9 class 0g
44	3, 43	cfv 6566	. . . . . . . 8 class (0g‘𝑓)
45	42, 34, 44	wsbc 3742	. . . . . . 7 wff [(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
46		cmulr 17473	. . . . . . . 8 class .r
47	3, 46	cfv 6566	. . . . . . 7 class (.r‘𝑓)
48	45, 17, 47	wsbc 3742	. . . . . 6 wff [(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
49		cplusg 17472	. . . . . . 7 class +g
50	3, 49	cfv 6566	. . . . . 6 class (+g‘𝑓)
51	48, 14, 50	wsbc 3742	. . . . 5 wff [(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
52		cbs 17431	. . . . . 6 class Base
53	3, 52	cfv 6566	. . . . 5 class (Base‘𝑓)
54	51, 30, 53	wsbc 3742	. . . 4 wff [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
55	7, 54	wa 401	. . 3 wff ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))
56		ccmn 20045	. . 3 class CMnd
57	55, 2, 56	crab 3416	. 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  20465