Definition df-srg 13145

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, 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 13144	. 2 class SRing
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1352	. . . . . 6 class 𝑓
4		cmgp 13128	. . . . . 6 class mulGrp
5	3, 4	cfv 5216	. . . . 5 class (mulGrp‘𝑓)
6		cmnd 12816	. . . . 5 class Mnd
7	5, 6	wcel 2148	. . . 4 wff (mulGrp‘𝑓) ∈ Mnd
8		vx	. . . . . . . . . . . . . . . 16 setvar 𝑥
9	8	cv 1352	. . . . . . . . . . . . . . 15 class 𝑥
10		vy	. . . . . . . . . . . . . . . . 17 setvar 𝑦
11	10	cv 1352	. . . . . . . . . . . . . . . 16 class 𝑦
12		vz	. . . . . . . . . . . . . . . . 17 setvar 𝑧
13	12	cv 1352	. . . . . . . . . . . . . . . 16 class 𝑧
14		vp	. . . . . . . . . . . . . . . . 17 setvar 𝑝
15	14	cv 1352	. . . . . . . . . . . . . . . 16 class 𝑝
16	11, 13, 15	co 5874	. . . . . . . . . . . . . . 15 class (𝑦𝑝𝑧)
17		vt	. . . . . . . . . . . . . . . 16 setvar 𝑡
18	17	cv 1352	. . . . . . . . . . . . . . 15 class 𝑡
19	9, 16, 18	co 5874	. . . . . . . . . . . . . 14 class (𝑥𝑡(𝑦𝑝𝑧))
20	9, 11, 18	co 5874	. . . . . . . . . . . . . . 15 class (𝑥𝑡𝑦)
21	9, 13, 18	co 5874	. . . . . . . . . . . . . . 15 class (𝑥𝑡𝑧)
22	20, 21, 15	co 5874	. . . . . . . . . . . . . 14 class ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
23	19, 22	wceq 1353	. . . . . . . . . . . . 13 wff (𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
24	9, 11, 15	co 5874	. . . . . . . . . . . . . . 15 class (𝑥𝑝𝑦)
25	24, 13, 18	co 5874	. . . . . . . . . . . . . 14 class ((𝑥𝑝𝑦)𝑡𝑧)
26	11, 13, 18	co 5874	. . . . . . . . . . . . . . 15 class (𝑦𝑡𝑧)
27	21, 26, 15	co 5874	. . . . . . . . . . . . . 14 class ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
28	25, 27	wceq 1353	. . . . . . . . . . . . 13 wff ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
29	23, 28	wa 104	. . . . . . . . . . . 12 wff ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
30		vr	. . . . . . . . . . . . 13 setvar 𝑟
31	30	cv 1352	. . . . . . . . . . . 12 class 𝑟
32	29, 12, 31	wral 2455	. . . . . . . . . . 11 wff ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
33	32, 10, 31	wral 2455	. . . . . . . . . 10 wff ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
34		vn	. . . . . . . . . . . . . 14 setvar 𝑛
35	34	cv 1352	. . . . . . . . . . . . 13 class 𝑛
36	35, 9, 18	co 5874	. . . . . . . . . . . 12 class (𝑛𝑡𝑥)
37	36, 35	wceq 1353	. . . . . . . . . . 11 wff (𝑛𝑡𝑥) = 𝑛
38	9, 35, 18	co 5874	. . . . . . . . . . . 12 class (𝑥𝑡𝑛)
39	38, 35	wceq 1353	. . . . . . . . . . 11 wff (𝑥𝑡𝑛) = 𝑛
40	37, 39	wa 104	. . . . . . . . . 10 wff ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)
41	33, 40	wa 104	. . . . . . . . 9 wff (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
42	41, 8, 31	wral 2455	. . . . . . . 8 wff ∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
43		c0g 12704	. . . . . . . . 9 class 0g
44	3, 43	cfv 5216	. . . . . . . 8 class (0g‘𝑓)
45	42, 34, 44	wsbc 2962	. . . . . . 7 wff [(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
46		cmulr 12536	. . . . . . . 8 class .r
47	3, 46	cfv 5216	. . . . . . 7 class (.r‘𝑓)
48	45, 17, 47	wsbc 2962	. . . . . 6 wff [(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
49		cplusg 12535	. . . . . . 7 class +g
50	3, 49	cfv 5216	. . . . . 6 class (+g‘𝑓)
51	48, 14, 50	wsbc 2962	. . . . 5 wff [(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
52		cbs 12461	. . . . . 6 class Base
53	3, 52	cfv 5216	. . . . 5 class (Base‘𝑓)
54	51, 30, 53	wsbc 2962	. . . 4 wff [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
55	7, 54	wa 104	. . 3 wff ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))
56		ccmn 13086	. . 3 class CMnd
57	55, 2, 56	crab 2459	. 2 class {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
58	1, 57	wceq 1353	1 wff SRing = {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}

This definition is referenced by:  issrg  13146