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

Definition df-srg 13078
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 13077 . 2  class SRing
2 vf . . . . . . 7  setvar  f
32cv 1352 . . . . . 6  class  f
4 cmgp 13061 . . . . . 6  class mulGrp
53, 4cfv 5215 . . . . 5  class  (mulGrp `  f )
6 cmnd 12749 . . . . 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 5872 . . . . . . . . . . . . . . 15  class  ( y p z )
17 vt . . . . . . . . . . . . . . . 16  setvar  t
1817cv 1352 . . . . . . . . . . . . . . 15  class  t
199, 16, 18co 5872 . . . . . . . . . . . . . 14  class  ( x t ( y p z ) )
209, 11, 18co 5872 . . . . . . . . . . . . . . 15  class  ( x t y )
219, 13, 18co 5872 . . . . . . . . . . . . . . 15  class  ( x t z )
2220, 21, 15co 5872 . . . . . . . . . . . . . 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 5872 . . . . . . . . . . . . . . 15  class  ( x p y )
2524, 13, 18co 5872 . . . . . . . . . . . . . 14  class  ( ( x p y ) t z )
2611, 13, 18co 5872 . . . . . . . . . . . . . . 15  class  ( y t z )
2721, 26, 15co 5872 . . . . . . . . . . . . . 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 5872 . . . . . . . . . . . 12  class  ( n t x )
3736, 35wceq 1353 . . . . . . . . . . 11  wff  ( n t x )  =  n
389, 35, 18co 5872 . . . . . . . . . . . 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 12693 . . . . . . . . 9  class  0g
443, 43cfv 5215 . . . . . . . 8  class  ( 0g
`  f )
4542, 34, 44wsbc 2962 . . . . . . 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 12529 . . . . . . . 8  class  .r
473, 46cfv 5215 . . . . . . 7  class  ( .r
`  f )
4845, 17, 47wsbc 2962 . . . . . 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 12528 . . . . . . 7  class  +g
503, 49cfv 5215 . . . . . 6  class  ( +g  `  f )
5148, 14, 50wsbc 2962 . . . . 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 12454 . . . . . 6  class  Base
533, 52cfv 5215 . . . . 5  class  ( Base `  f )
5451, 30, 53wsbc 2962 . . . 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 13019 . . 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  13079
  Copyright terms: Public domain W3C validator