Definition df-srg 13927

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 13926	. 2 class SRing
2		vf	. . . . . . 7 setvar f
3	2	cv 1394	. . . . . 6 class f
4		cmgp 13883	. . . . . 6 class mulGrp
5	3, 4	cfv 5318	. . . . 5 class (mulGrp ` f )
6		cmnd 13449	. . . . 5 class Mnd
7	5, 6	wcel 2200	. . . 4 wff (mulGrp ` f ) e. Mnd
8		vx	. . . . . . . . . . . . . . . 16 setvar x
9	8	cv 1394	. . . . . . . . . . . . . . 15 class x
10		vy	. . . . . . . . . . . . . . . . 17 setvar y
11	10	cv 1394	. . . . . . . . . . . . . . . 16 class y
12		vz	. . . . . . . . . . . . . . . . 17 setvar z
13	12	cv 1394	. . . . . . . . . . . . . . . 16 class z
14		vp	. . . . . . . . . . . . . . . . 17 setvar p
15	14	cv 1394	. . . . . . . . . . . . . . . 16 class p
16	11, 13, 15	co 6001	. . . . . . . . . . . . . . 15 class ( y p z )
17		vt	. . . . . . . . . . . . . . . 16 setvar t
18	17	cv 1394	. . . . . . . . . . . . . . 15 class t
19	9, 16, 18	co 6001	. . . . . . . . . . . . . 14 class ( x t ( y p z ) )
20	9, 11, 18	co 6001	. . . . . . . . . . . . . . 15 class ( x t y )
21	9, 13, 18	co 6001	. . . . . . . . . . . . . . 15 class ( x t z )
22	20, 21, 15	co 6001	. . . . . . . . . . . . . 14 class ( ( x t y ) p ( x t z ) )
23	19, 22	wceq 1395	. . . . . . . . . . . . 13 wff ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) )
24	9, 11, 15	co 6001	. . . . . . . . . . . . . . 15 class ( x p y )
25	24, 13, 18	co 6001	. . . . . . . . . . . . . 14 class ( ( x p y ) t z )
26	11, 13, 18	co 6001	. . . . . . . . . . . . . . 15 class ( y t z )
27	21, 26, 15	co 6001	. . . . . . . . . . . . . 14 class ( ( x t z ) p ( y t z ) )
28	25, 27	wceq 1395	. . . . . . . . . . . . 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 1394	. . . . . . . . . . . 12 class r
32	29, 12, 31	wral 2508	. . . . . . . . . . 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 2508	. . . . . . . . . 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 1394	. . . . . . . . . . . . 13 class n
36	35, 9, 18	co 6001	. . . . . . . . . . . 12 class ( n t x )
37	36, 35	wceq 1395	. . . . . . . . . . 11 wff ( n t x ) = n
38	9, 35, 18	co 6001	. . . . . . . . . . . 12 class ( x t n )
39	38, 35	wceq 1395	. . . . . . . . . . 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 2508	. . . . . . . 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 13289	. . . . . . . . 9 class 0g
44	3, 43	cfv 5318	. . . . . . . 8 class ( 0g ` f )
45	42, 34, 44	wsbc 3028	. . . . . . 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 13111	. . . . . . . 8 class .r
47	3, 46	cfv 5318	. . . . . . 7 class ( .r ` f )
48	45, 17, 47	wsbc 3028	. . . . . 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 13110	. . . . . . 7 class +g
50	3, 49	cfv 5318	. . . . . 6 class ( +g ` f )
51	48, 14, 50	wsbc 3028	. . . . 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 13032	. . . . . 6 class Base
53	3, 52	cfv 5318	. . . . 5 class ( Base ` f )
54	51, 30, 53	wsbc 3028	. . . 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 13821	. . 3 class CMnd
57	55, 2, 56	crab 2512	. 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 1395	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  13928