Definition df-srg 20100

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 20148), 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 20099	. 2 class SRing
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1540	. . . . . 6 class 𝑓
4		cmgp 20053	. . . . . 6 class mulGrp
5	3, 4	cfv 6476	. . . . 5 class (mulGrp‘𝑓)
6		cmnd 18637	. . . . 5 class Mnd
7	5, 6	wcel 2111	. . . 4 wff (mulGrp‘𝑓) ∈ Mnd
8		vx	. . . . . . . . . . . . . . . 16 setvar 𝑥
9	8	cv 1540	. . . . . . . . . . . . . . 15 class 𝑥
10		vy	. . . . . . . . . . . . . . . . 17 setvar 𝑦
11	10	cv 1540	. . . . . . . . . . . . . . . 16 class 𝑦
12		vz	. . . . . . . . . . . . . . . . 17 setvar 𝑧
13	12	cv 1540	. . . . . . . . . . . . . . . 16 class 𝑧
14		vp	. . . . . . . . . . . . . . . . 17 setvar 𝑝
15	14	cv 1540	. . . . . . . . . . . . . . . 16 class 𝑝
16	11, 13, 15	co 7341	. . . . . . . . . . . . . . 15 class (𝑦𝑝𝑧)
17		vt	. . . . . . . . . . . . . . . 16 setvar 𝑡
18	17	cv 1540	. . . . . . . . . . . . . . 15 class 𝑡
19	9, 16, 18	co 7341	. . . . . . . . . . . . . 14 class (𝑥𝑡(𝑦𝑝𝑧))
20	9, 11, 18	co 7341	. . . . . . . . . . . . . . 15 class (𝑥𝑡𝑦)
21	9, 13, 18	co 7341	. . . . . . . . . . . . . . 15 class (𝑥𝑡𝑧)
22	20, 21, 15	co 7341	. . . . . . . . . . . . . 14 class ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
23	19, 22	wceq 1541	. . . . . . . . . . . . 13 wff (𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
24	9, 11, 15	co 7341	. . . . . . . . . . . . . . 15 class (𝑥𝑝𝑦)
25	24, 13, 18	co 7341	. . . . . . . . . . . . . 14 class ((𝑥𝑝𝑦)𝑡𝑧)
26	11, 13, 18	co 7341	. . . . . . . . . . . . . . 15 class (𝑦𝑡𝑧)
27	21, 26, 15	co 7341	. . . . . . . . . . . . . 14 class ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
28	25, 27	wceq 1541	. . . . . . . . . . . . 13 wff ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
29	23, 28	wa 395	. . . . . . . . . . . 12 wff ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
30		vr	. . . . . . . . . . . . 13 setvar 𝑟
31	30	cv 1540	. . . . . . . . . . . 12 class 𝑟
32	29, 12, 31	wral 3047	. . . . . . . . . . 11 wff ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
33	32, 10, 31	wral 3047	. . . . . . . . . 10 wff ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
34		vn	. . . . . . . . . . . . . 14 setvar 𝑛
35	34	cv 1540	. . . . . . . . . . . . 13 class 𝑛
36	35, 9, 18	co 7341	. . . . . . . . . . . 12 class (𝑛𝑡𝑥)
37	36, 35	wceq 1541	. . . . . . . . . . 11 wff (𝑛𝑡𝑥) = 𝑛
38	9, 35, 18	co 7341	. . . . . . . . . . . 12 class (𝑥𝑡𝑛)
39	38, 35	wceq 1541	. . . . . . . . . . 11 wff (𝑥𝑡𝑛) = 𝑛
40	37, 39	wa 395	. . . . . . . . . 10 wff ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)
41	33, 40	wa 395	. . . . . . . . 9 wff (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
42	41, 8, 31	wral 3047	. . . . . . . 8 wff ∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
43		c0g 17338	. . . . . . . . 9 class 0g
44	3, 43	cfv 6476	. . . . . . . 8 class (0g‘𝑓)
45	42, 34, 44	wsbc 3736	. . . . . . 7 wff [(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
46		cmulr 17157	. . . . . . . 8 class .r
47	3, 46	cfv 6476	. . . . . . 7 class (.r‘𝑓)
48	45, 17, 47	wsbc 3736	. . . . . 6 wff [(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
49		cplusg 17156	. . . . . . 7 class +g
50	3, 49	cfv 6476	. . . . . 6 class (+g‘𝑓)
51	48, 14, 50	wsbc 3736	. . . . 5 wff [(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
52		cbs 17115	. . . . . 6 class Base
53	3, 52	cfv 6476	. . . . 5 class (Base‘𝑓)
54	51, 30, 53	wsbc 3736	. . . 4 wff [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
55	7, 54	wa 395	. . 3 wff ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))
56		ccmn 19687	. . 3 class CMnd
57	55, 2, 56	crab 3395	. 2 class {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
58	1, 57	wceq 1541	1 wff SRing = {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}

This definition is referenced by:  issrg  20101