Definition df-srg 14268

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 14267	. 2 class SRing
2		vf	. . . . . . 7 setvar f
3	2	cv 1401	. . . . . 6 class f
4		cmgp 14217	. . . . . 6 class mulGrp
5	3, 4	cfv 5377	. . . . 5 class (mulGrp ` f )
6		cmnd 13729	. . . . 5 class Mnd
7	5, 6	wcel 2209	. . . 4 wff (mulGrp ` f ) e. Mnd
8		vx	. . . . . . . . . . . . . . . 16 setvar x
9	8	cv 1401	. . . . . . . . . . . . . . 15 class x
10		vy	. . . . . . . . . . . . . . . . 17 setvar y
11	10	cv 1401	. . . . . . . . . . . . . . . 16 class y
12		vz	. . . . . . . . . . . . . . . . 17 setvar z
13	12	cv 1401	. . . . . . . . . . . . . . . 16 class z
14		vp	. . . . . . . . . . . . . . . . 17 setvar p
15	14	cv 1401	. . . . . . . . . . . . . . . 16 class p
16	11, 13, 15	co 6085	. . . . . . . . . . . . . . 15 class ( y p z )
17		vt	. . . . . . . . . . . . . . . 16 setvar t
18	17	cv 1401	. . . . . . . . . . . . . . 15 class t
19	9, 16, 18	co 6085	. . . . . . . . . . . . . 14 class ( x t ( y p z ) )
20	9, 11, 18	co 6085	. . . . . . . . . . . . . . 15 class ( x t y )
21	9, 13, 18	co 6085	. . . . . . . . . . . . . . 15 class ( x t z )
22	20, 21, 15	co 6085	. . . . . . . . . . . . . 14 class ( ( x t y ) p ( x t z ) )
23	19, 22	wceq 1402	. . . . . . . . . . . . 13 wff ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) )
24	9, 11, 15	co 6085	. . . . . . . . . . . . . . 15 class ( x p y )
25	24, 13, 18	co 6085	. . . . . . . . . . . . . 14 class ( ( x p y ) t z )
26	11, 13, 18	co 6085	. . . . . . . . . . . . . . 15 class ( y t z )
27	21, 26, 15	co 6085	. . . . . . . . . . . . . 14 class ( ( x t z ) p ( y t z ) )
28	25, 27	wceq 1402	. . . . . . . . . . . . 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 1401	. . . . . . . . . . . 12 class r
32	29, 12, 31	wral 2528	. . . . . . . . . . 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 2528	. . . . . . . . . 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 1401	. . . . . . . . . . . . 13 class n
36	35, 9, 18	co 6085	. . . . . . . . . . . 12 class ( n t x )
37	36, 35	wceq 1402	. . . . . . . . . . 11 wff ( n t x ) = n
38	9, 35, 18	co 6085	. . . . . . . . . . . 12 class ( x t n )
39	38, 35	wceq 1402	. . . . . . . . . . 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 2528	. . . . . . . 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 13610	. . . . . . . . 9 class 0g
44	3, 43	cfv 5377	. . . . . . . 8 class ( 0g ` f )
45	42, 34, 44	wsbc 3051	. . . . . . 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 13432	. . . . . . . 8 class .r
47	3, 46	cfv 5377	. . . . . . 7 class ( .r ` f )
48	45, 17, 47	wsbc 3051	. . . . . 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 13431	. . . . . . 7 class +g
50	3, 49	cfv 5377	. . . . . 6 class ( +g ` f )
51	48, 14, 50	wsbc 3051	. . . . 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 13352	. . . . . 6 class Base
53	3, 52	cfv 5377	. . . . 5 class ( Base ` f )
54	51, 30, 53	wsbc 3051	. . . 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 14087	. . 3 class CMnd
57	55, 2, 56	crab 2532	. 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 1402	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 used by:  issrg  14269