Definition df-srg 13841

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 = { f e. CMnd | ( (mulGrp ` f ) e. Mnd /\ [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. [. ( 0g ` f ) / n ]. A. x e. r ( A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) /\ ( ( n t x ) = n /\ ( x t n ) = n ) ) ) }

Distinct variable group:   f, n, p, r, t, x, y, z

Detailed syntax breakdown of Definition df-srg

Step	Hyp	Ref	Expression
1		csrg 13840	. 2 class SRing
2		vf	. . . . . . 7 setvar f
3	2	cv 1372	. . . . . 6 class f
4		cmgp 13797	. . . . . 6 class mulGrp
5	3, 4	cfv 5290	. . . . 5 class (mulGrp ` f )
6		cmnd 13363	. . . . 5 class Mnd
7	5, 6	wcel 2178	. . . 4 wff (mulGrp ` f ) e. Mnd
8		vx	. . . . . . . . . . . . . . . 16 setvar x
9	8	cv 1372	. . . . . . . . . . . . . . 15 class x
10		vy	. . . . . . . . . . . . . . . . 17 setvar y
11	10	cv 1372	. . . . . . . . . . . . . . . 16 class y
12		vz	. . . . . . . . . . . . . . . . 17 setvar z
13	12	cv 1372	. . . . . . . . . . . . . . . 16 class z
14		vp	. . . . . . . . . . . . . . . . 17 setvar p
15	14	cv 1372	. . . . . . . . . . . . . . . 16 class p
16	11, 13, 15	co 5967	. . . . . . . . . . . . . . 15 class ( y p z )
17		vt	. . . . . . . . . . . . . . . 16 setvar t
18	17	cv 1372	. . . . . . . . . . . . . . 15 class t
19	9, 16, 18	co 5967	. . . . . . . . . . . . . 14 class ( x t ( y p z ) )
20	9, 11, 18	co 5967	. . . . . . . . . . . . . . 15 class ( x t y )
21	9, 13, 18	co 5967	. . . . . . . . . . . . . . 15 class ( x t z )
22	20, 21, 15	co 5967	. . . . . . . . . . . . . 14 class ( ( x t y ) p ( x t z ) )
23	19, 22	wceq 1373	. . . . . . . . . . . . 13 wff ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) )
24	9, 11, 15	co 5967	. . . . . . . . . . . . . . 15 class ( x p y )
25	24, 13, 18	co 5967	. . . . . . . . . . . . . 14 class ( ( x p y ) t z )
26	11, 13, 18	co 5967	. . . . . . . . . . . . . . 15 class ( y t z )
27	21, 26, 15	co 5967	. . . . . . . . . . . . . 14 class ( ( x t z ) p ( y t z ) )
28	25, 27	wceq 1373	. . . . . . . . . . . . 13 wff ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) )
29	23, 28	wa 104	. . . . . . . . . . . 12 wff ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) )
30		vr	. . . . . . . . . . . . 13 setvar r
31	30	cv 1372	. . . . . . . . . . . 12 class r
32	29, 12, 31	wral 2486	. . . . . . . . . . 11 wff A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) )
33	32, 10, 31	wral 2486	. . . . . . . . . 10 wff A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) )
34		vn	. . . . . . . . . . . . . 14 setvar n
35	34	cv 1372	. . . . . . . . . . . . 13 class n
36	35, 9, 18	co 5967	. . . . . . . . . . . 12 class ( n t x )
37	36, 35	wceq 1373	. . . . . . . . . . 11 wff ( n t x ) = n
38	9, 35, 18	co 5967	. . . . . . . . . . . 12 class ( x t n )
39	38, 35	wceq 1373	. . . . . . . . . . 11 wff ( x t n ) = n
40	37, 39	wa 104	. . . . . . . . . 10 wff ( ( n t x ) = n /\ ( x t n ) = n )
41	33, 40	wa 104	. . . . . . . . 9 wff ( A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) /\ ( ( n t x ) = n /\ ( x t n ) = n ) )
42	41, 8, 31	wral 2486	. . . . . . . 8 wff A. x e. r ( A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) /\ ( ( n t x ) = n /\ ( x t n ) = n ) )
43		c0g 13203	. . . . . . . . 9 class 0g
44	3, 43	cfv 5290	. . . . . . . 8 class ( 0g ` f )
45	42, 34, 44	wsbc 3005	. . . . . . 7 wff [. ( 0g ` f ) / n ]. A. x e. r ( A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) /\ ( ( n t x ) = n /\ ( x t n ) = n ) )
46		cmulr 13025	. . . . . . . 8 class .r
47	3, 46	cfv 5290	. . . . . . 7 class ( .r ` f )
48	45, 17, 47	wsbc 3005	. . . . . 6 wff [. ( .r ` f ) / t ]. [. ( 0g ` f ) / n ]. A. x e. r ( A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) /\ ( ( n t x ) = n /\ ( x t n ) = n ) )
49		cplusg 13024	. . . . . . 7 class +g
50	3, 49	cfv 5290	. . . . . 6 class ( +g ` f )
51	48, 14, 50	wsbc 3005	. . . . 5 wff [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. [. ( 0g ` f ) / n ]. A. x e. r ( A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) /\ ( ( n t x ) = n /\ ( x t n ) = n ) )
52		cbs 12947	. . . . . 6 class Base
53	3, 52	cfv 5290	. . . . 5 class ( Base ` f )
54	51, 30, 53	wsbc 3005	. . . 4 wff [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. [. ( 0g ` f ) / n ]. A. x e. r ( A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) /\ ( ( n t x ) = n /\ ( x t n ) = n ) )
55	7, 54	wa 104	. . 3 wff ( (mulGrp ` f ) e. Mnd /\ [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. [. ( 0g ` f ) / n ]. A. x e. r ( A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) /\ ( ( n t x ) = n /\ ( x t n ) = n ) ) )
56		ccmn 13735	. . 3 class CMnd
57	55, 2, 56	crab 2490	. 2 class { f e. CMnd | ( (mulGrp ` f ) e. Mnd /\ [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. [. ( 0g ` f ) / n ]. A. x e. r ( A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) /\ ( ( n t x ) = n /\ ( x t n ) = n ) ) ) }
58	1, 57	wceq 1373	1 wff SRing = { f e. CMnd | ( (mulGrp ` f ) e. Mnd /\ [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. [. ( 0g ` f ) / n ]. A. x e. r ( A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) /\ ( ( n t x ) = n /\ ( x t n ) = n ) ) ) }

This definition is referenced by:  issrg  13842