Definition df-srg 14375

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 14374	. 2 class SRing
2		vf	. . . . . . 7 setvar f
3	2	cv 1401	. . . . . 6 class f
4		cmgp 14324	. . . . . 6 class mulGrp
5	3, 4	cfv 5380	. . . . 5 class (mulGrp ` f )
6		cmnd 13788	. . . . 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 6088	. . . . . . . . . . . . . . 15 class ( y p z )
17		vt	. . . . . . . . . . . . . . . 16 setvar t
18	17	cv 1401	. . . . . . . . . . . . . . 15 class t
19	9, 16, 18	co 6088	. . . . . . . . . . . . . 14 class ( x t ( y p z ) )
20	9, 11, 18	co 6088	. . . . . . . . . . . . . . 15 class ( x t y )
21	9, 13, 18	co 6088	. . . . . . . . . . . . . . 15 class ( x t z )
22	20, 21, 15	co 6088	. . . . . . . . . . . . . 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 6088	. . . . . . . . . . . . . . 15 class ( x p y )
25	24, 13, 18	co 6088	. . . . . . . . . . . . . 14 class ( ( x p y ) t z )
26	11, 13, 18	co 6088	. . . . . . . . . . . . . . 15 class ( y t z )
27	21, 26, 15	co 6088	. . . . . . . . . . . . . 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 6088	. . . . . . . . . . . 12 class ( n t x )
37	36, 35	wceq 1402	. . . . . . . . . . 11 wff ( n t x ) = n
38	9, 35, 18	co 6088	. . . . . . . . . . . 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 13669	. . . . . . . . 9 class 0g
44	3, 43	cfv 5380	. . . . . . . 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 13491	. . . . . . . 8 class .r
47	3, 46	cfv 5380	. . . . . . 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 13490	. . . . . . 7 class +g
50	3, 49	cfv 5380	. . . . . 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 13410	. . . . . 6 class Base
53	3, 52	cfv 5380	. . . . 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 14177	. . 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  14376