MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-srg Structured version   Unicode version

Definition df-srg 16620
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. Compared to the definition of a ring, this definition also adds that the additive identity is an absorbing element of the multiplicative law, as this 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
StepHypRef Expression
1 csrg 16619 . 2  class SRing
2 vf . . . . . . 7  setvar  f
32cv 1368 . . . . . 6  class  f
4 cmgp 16603 . . . . . 6  class mulGrp
53, 4cfv 5430 . . . . 5  class  (mulGrp `  f )
6 cmnd 15421 . . . . 5  class  Mnd
75, 6wcel 1756 . . . 4  wff  (mulGrp `  f )  e.  Mnd
8 vx . . . . . . . . . . . . . . . 16  setvar  x
98cv 1368 . . . . . . . . . . . . . . 15  class  x
10 vy . . . . . . . . . . . . . . . . 17  setvar  y
1110cv 1368 . . . . . . . . . . . . . . . 16  class  y
12 vz . . . . . . . . . . . . . . . . 17  setvar  z
1312cv 1368 . . . . . . . . . . . . . . . 16  class  z
14 vp . . . . . . . . . . . . . . . . 17  setvar  p
1514cv 1368 . . . . . . . . . . . . . . . 16  class  p
1611, 13, 15co 6103 . . . . . . . . . . . . . . 15  class  ( y p z )
17 vt . . . . . . . . . . . . . . . 16  setvar  t
1817cv 1368 . . . . . . . . . . . . . . 15  class  t
199, 16, 18co 6103 . . . . . . . . . . . . . 14  class  ( x t ( y p z ) )
209, 11, 18co 6103 . . . . . . . . . . . . . . 15  class  ( x t y )
219, 13, 18co 6103 . . . . . . . . . . . . . . 15  class  ( x t z )
2220, 21, 15co 6103 . . . . . . . . . . . . . 14  class  ( ( x t y ) p ( x t z ) )
2319, 22wceq 1369 . . . . . . . . . . . . 13  wff  ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )
249, 11, 15co 6103 . . . . . . . . . . . . . . 15  class  ( x p y )
2524, 13, 18co 6103 . . . . . . . . . . . . . 14  class  ( ( x p y ) t z )
2611, 13, 18co 6103 . . . . . . . . . . . . . . 15  class  ( y t z )
2721, 26, 15co 6103 . . . . . . . . . . . . . 14  class  ( ( x t z ) p ( y t z ) )
2825, 27wceq 1369 . . . . . . . . . . . . 13  wff  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) )
2923, 28wa 369 . . . . . . . . . . . 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
3130cv 1368 . . . . . . . . . . . 12  class  r
3229, 12, 31wral 2727 . . . . . . . . . . 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 ) ) )
3332, 10, 31wral 2727 . . . . . . . . . 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
3534cv 1368 . . . . . . . . . . . . 13  class  n
3635, 9, 18co 6103 . . . . . . . . . . . 12  class  ( n t x )
3736, 35wceq 1369 . . . . . . . . . . 11  wff  ( n t x )  =  n
389, 35, 18co 6103 . . . . . . . . . . . 12  class  ( x t n )
3938, 35wceq 1369 . . . . . . . . . . 11  wff  ( x t n )  =  n
4037, 39wa 369 . . . . . . . . . 10  wff  ( ( n t x )  =  n  /\  (
x t n )  =  n )
4133, 40wa 369 . . . . . . . . 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 ) )
4241, 8, 31wral 2727 . . . . . . . 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 14390 . . . . . . . . 9  class  0g
443, 43cfv 5430 . . . . . . . 8  class  ( 0g
`  f )
4542, 34, 44wsbc 3198 . . . . . . 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 14251 . . . . . . . 8  class  .r
473, 46cfv 5430 . . . . . . 7  class  ( .r
`  f )
4845, 17, 47wsbc 3198 . . . . . 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 14250 . . . . . . 7  class  +g
503, 49cfv 5430 . . . . . 6  class  ( +g  `  f )
5148, 14, 50wsbc 3198 . . . . 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 14186 . . . . . 6  class  Base
533, 52cfv 5430 . . . . 5  class  ( Base `  f )
5451, 30, 53wsbc 3198 . . . 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 ) )
557, 54wa 369 . . 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 16289 . . 3  class CMnd
5755, 2, 56crab 2731 . 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 ) ) ) }
581, 57wceq 1369 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 ) ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  issrg  16621
  Copyright terms: Public domain W3C validator