Definition df-srg

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 ), 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)

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

Detailed syntax breakdown

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