Definition df-srg 13976

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 13975	. 2 class SRing
2		vf	. . . . . . 7 setvar f
3	2	cv 1396	. . . . . 6 class f
4		cmgp 13932	. . . . . 6 class mulGrp
5	3, 4	cfv 5326	. . . . 5 class (mulGrp ` f )
6		cmnd 13498	. . . . 5 class Mnd
7	5, 6	wcel 2202	. . . 4 wff (mulGrp ` f ) e. Mnd
8		vx	. . . . . . . . . . . . . . . 16 setvar x
9	8	cv 1396	. . . . . . . . . . . . . . 15 class x
10		vy	. . . . . . . . . . . . . . . . 17 setvar y
11	10	cv 1396	. . . . . . . . . . . . . . . 16 class y
12		vz	. . . . . . . . . . . . . . . . 17 setvar z
13	12	cv 1396	. . . . . . . . . . . . . . . 16 class z
14		vp	. . . . . . . . . . . . . . . . 17 setvar p
15	14	cv 1396	. . . . . . . . . . . . . . . 16 class p
16	11, 13, 15	co 6017	. . . . . . . . . . . . . . 15 class ( y p z )
17		vt	. . . . . . . . . . . . . . . 16 setvar t
18	17	cv 1396	. . . . . . . . . . . . . . 15 class t
19	9, 16, 18	co 6017	. . . . . . . . . . . . . 14 class ( x t ( y p z ) )
20	9, 11, 18	co 6017	. . . . . . . . . . . . . . 15 class ( x t y )
21	9, 13, 18	co 6017	. . . . . . . . . . . . . . 15 class ( x t z )
22	20, 21, 15	co 6017	. . . . . . . . . . . . . 14 class ( ( x t y ) p ( x t z ) )
23	19, 22	wceq 1397	. . . . . . . . . . . . 13 wff ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) )
24	9, 11, 15	co 6017	. . . . . . . . . . . . . . 15 class ( x p y )
25	24, 13, 18	co 6017	. . . . . . . . . . . . . 14 class ( ( x p y ) t z )
26	11, 13, 18	co 6017	. . . . . . . . . . . . . . 15 class ( y t z )
27	21, 26, 15	co 6017	. . . . . . . . . . . . . 14 class ( ( x t z ) p ( y t z ) )
28	25, 27	wceq 1397	. . . . . . . . . . . . 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 1396	. . . . . . . . . . . 12 class r
32	29, 12, 31	wral 2510	. . . . . . . . . . 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 2510	. . . . . . . . . 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 1396	. . . . . . . . . . . . 13 class n
36	35, 9, 18	co 6017	. . . . . . . . . . . 12 class ( n t x )
37	36, 35	wceq 1397	. . . . . . . . . . 11 wff ( n t x ) = n
38	9, 35, 18	co 6017	. . . . . . . . . . . 12 class ( x t n )
39	38, 35	wceq 1397	. . . . . . . . . . 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 2510	. . . . . . . 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 13338	. . . . . . . . 9 class 0g
44	3, 43	cfv 5326	. . . . . . . 8 class ( 0g ` f )
45	42, 34, 44	wsbc 3031	. . . . . . 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 13160	. . . . . . . 8 class .r
47	3, 46	cfv 5326	. . . . . . 7 class ( .r ` f )
48	45, 17, 47	wsbc 3031	. . . . . 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 13159	. . . . . . 7 class +g
50	3, 49	cfv 5326	. . . . . 6 class ( +g ` f )
51	48, 14, 50	wsbc 3031	. . . . 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 13081	. . . . . 6 class Base
53	3, 52	cfv 5326	. . . . 5 class ( Base ` f )
54	51, 30, 53	wsbc 3031	. . . 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 13870	. . 3 class CMnd
57	55, 2, 56	crab 2514	. 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 1397	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  13977