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. Compared to the definition of a ring, this definition also adds that the additive identity is an absorbing element of the multiplicative law, as this 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 ‘ 𝑓 ) / 𝑛 ] ∀ 𝑥 ∈ 𝑟 ( ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ) }