ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-srg Unicode version

Definition df-srg 13152
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
StepHypRef Expression
1 csrg 13151 . 2  class SRing
2 vf . . . . . . 7  setvar  f
32cv 1352 . . . . . 6  class  f
4 cmgp 13135 . . . . . 6  class mulGrp
53, 4cfv 5218 . . . . 5  class  (mulGrp `  f )
6 cmnd 12822 . . . . 5  class  Mnd
75, 6wcel 2148 . . . 4  wff  (mulGrp `  f )  e.  Mnd
8 vx . . . . . . . . . . . . . . . 16  setvar  x
98cv 1352 . . . . . . . . . . . . . . 15  class  x
10 vy . . . . . . . . . . . . . . . . 17  setvar  y
1110cv 1352 . . . . . . . . . . . . . . . 16  class  y
12 vz . . . . . . . . . . . . . . . . 17  setvar  z
1312cv 1352 . . . . . . . . . . . . . . . 16  class  z
14 vp . . . . . . . . . . . . . . . . 17  setvar  p
1514cv 1352 . . . . . . . . . . . . . . . 16  class  p
1611, 13, 15co 5877 . . . . . . . . . . . . . . 15  class  ( y p z )
17 vt . . . . . . . . . . . . . . . 16  setvar  t
1817cv 1352 . . . . . . . . . . . . . . 15  class  t
199, 16, 18co 5877 . . . . . . . . . . . . . 14  class  ( x t ( y p z ) )
209, 11, 18co 5877 . . . . . . . . . . . . . . 15  class  ( x t y )
219, 13, 18co 5877 . . . . . . . . . . . . . . 15  class  ( x t z )
2220, 21, 15co 5877 . . . . . . . . . . . . . 14  class  ( ( x t y ) p ( x t z ) )
2319, 22wceq 1353 . . . . . . . . . . . . 13  wff  ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )
249, 11, 15co 5877 . . . . . . . . . . . . . . 15  class  ( x p y )
2524, 13, 18co 5877 . . . . . . . . . . . . . 14  class  ( ( x p y ) t z )
2611, 13, 18co 5877 . . . . . . . . . . . . . . 15  class  ( y t z )
2721, 26, 15co 5877 . . . . . . . . . . . . . 14  class  ( ( x t z ) p ( y t z ) )
2825, 27wceq 1353 . . . . . . . . . . . . 13  wff  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) )
2923, 28wa 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
3130cv 1352 . . . . . . . . . . . 12  class  r
3229, 12, 31wral 2455 . . . . . . . . . . 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 2455 . . . . . . . . . 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 1352 . . . . . . . . . . . . 13  class  n
3635, 9, 18co 5877 . . . . . . . . . . . 12  class  ( n t x )
3736, 35wceq 1353 . . . . . . . . . . 11  wff  ( n t x )  =  n
389, 35, 18co 5877 . . . . . . . . . . . 12  class  ( x t n )
3938, 35wceq 1353 . . . . . . . . . . 11  wff  ( x t n )  =  n
4037, 39wa 104 . . . . . . . . . 10  wff  ( ( n t x )  =  n  /\  (
x t n )  =  n )
4133, 40wa 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 ) )
4241, 8, 31wral 2455 . . . . . . . 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 12710 . . . . . . . . 9  class  0g
443, 43cfv 5218 . . . . . . . 8  class  ( 0g
`  f )
4542, 34, 44wsbc 2964 . . . . . . 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 12539 . . . . . . . 8  class  .r
473, 46cfv 5218 . . . . . . 7  class  ( .r
`  f )
4845, 17, 47wsbc 2964 . . . . . 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 12538 . . . . . . 7  class  +g
503, 49cfv 5218 . . . . . 6  class  ( +g  `  f )
5148, 14, 50wsbc 2964 . . . . 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 12464 . . . . . 6  class  Base
533, 52cfv 5218 . . . . 5  class  ( Base `  f )
5451, 30, 53wsbc 2964 . . . 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 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 13093 . . 3  class CMnd
5755, 2, 56crab 2459 . 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 1353 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 set class
This definition is referenced by:  issrg  13153
  Copyright terms: Public domain W3C validator