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

Definition df-rng 15356
Description: Define class of all (unital) rings. A unital ring is a set equipped with two everywhere-defined internal operations, whose first one is an additive group structure and the second one is a multiplicative monoid structure, and where the addition is left- and right-distributive for the multiplication. So that the additive structure must be abelian (see rngcom 15385), care must be taken that in the case of a non-unital ring, the commutativity of addition must be postulated and cannot be proved from the other conditions. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 27-Dec-2014.)
Assertion
Ref Expression
df-rng  |-  Ring  =  { f  e.  Grp  |  ( (mulGrp `  f
)  e.  Mnd  /\  [. ( Base `  f
)  /  r ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. 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 ) ) ) ) }
Distinct variable group:    f, p, r, t, x, y, z

Detailed syntax breakdown of Definition df-rng
StepHypRef Expression
1 crg 15353 . 2  class  Ring
2 vf . . . . . . 7  set  f
32cv 1631 . . . . . 6  class  f
4 cmgp 15341 . . . . . 6  class mulGrp
53, 4cfv 5271 . . . . 5  class  (mulGrp `  f )
6 cmnd 14377 . . . . 5  class  Mnd
75, 6wcel 1696 . . . 4  wff  (mulGrp `  f )  e.  Mnd
8 vx . . . . . . . . . . . . . 14  set  x
98cv 1631 . . . . . . . . . . . . 13  class  x
10 vy . . . . . . . . . . . . . . 15  set  y
1110cv 1631 . . . . . . . . . . . . . 14  class  y
12 vz . . . . . . . . . . . . . . 15  set  z
1312cv 1631 . . . . . . . . . . . . . 14  class  z
14 vp . . . . . . . . . . . . . . 15  set  p
1514cv 1631 . . . . . . . . . . . . . 14  class  p
1611, 13, 15co 5874 . . . . . . . . . . . . 13  class  ( y p z )
17 vt . . . . . . . . . . . . . 14  set  t
1817cv 1631 . . . . . . . . . . . . 13  class  t
199, 16, 18co 5874 . . . . . . . . . . . 12  class  ( x t ( y p z ) )
209, 11, 18co 5874 . . . . . . . . . . . . 13  class  ( x t y )
219, 13, 18co 5874 . . . . . . . . . . . . 13  class  ( x t z )
2220, 21, 15co 5874 . . . . . . . . . . . 12  class  ( ( x t y ) p ( x t z ) )
2319, 22wceq 1632 . . . . . . . . . . 11  wff  ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )
249, 11, 15co 5874 . . . . . . . . . . . . 13  class  ( x p y )
2524, 13, 18co 5874 . . . . . . . . . . . 12  class  ( ( x p y ) t z )
2611, 13, 18co 5874 . . . . . . . . . . . . 13  class  ( y t z )
2721, 26, 15co 5874 . . . . . . . . . . . 12  class  ( ( x t z ) p ( y t z ) )
2825, 27wceq 1632 . . . . . . . . . . 11  wff  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) )
2923, 28wa 358 . . . . . . . . . 10  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 . . . . . . . . . . 11  set  r
3130cv 1631 . . . . . . . . . 10  class  r
3229, 12, 31wral 2556 . . . . . . . . 9  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 2556 . . . . . . . 8  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 ) ) )
3433, 8, 31wral 2556 . . . . . . 7  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 ) ) )
35 cmulr 13225 . . . . . . . 8  class  .r
363, 35cfv 5271 . . . . . . 7  class  ( .r
`  f )
3734, 17, 36wsbc 3004 . . . . . 6  wff  [. ( .r `  f )  / 
t ]. 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 ) ) )
38 cplusg 13224 . . . . . . 7  class  +g
393, 38cfv 5271 . . . . . 6  class  ( +g  `  f )
4037, 14, 39wsbc 3004 . . . . 5  wff  [. ( +g  `  f )  /  p ]. [. ( .r
`  f )  / 
t ]. 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 ) ) )
41 cbs 13164 . . . . . 6  class  Base
423, 41cfv 5271 . . . . 5  class  ( Base `  f )
4340, 30, 42wsbc 3004 . . . 4  wff  [. ( Base `  f )  / 
r ]. [. ( +g  `  f )  /  p ]. [. ( .r `  f )  /  t ]. 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 ) ) )
447, 43wa 358 . . 3  wff  ( (mulGrp `  f )  e.  Mnd  /\ 
[. ( Base `  f
)  /  r ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. 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 ) ) ) )
45 cgrp 14378 . . 3  class  Grp
4644, 2, 45crab 2560 . 2  class  { f  e.  Grp  |  ( (mulGrp `  f )  e.  Mnd  /\  [. ( Base `  f )  / 
r ]. [. ( +g  `  f )  /  p ]. [. ( .r `  f )  /  t ]. 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 ) ) ) ) }
471, 46wceq 1632 1  wff  Ring  =  { f  e.  Grp  |  ( (mulGrp `  f
)  e.  Mnd  /\  [. ( Base `  f
)  /  r ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. 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 ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  isrng  15361
  Copyright terms: Public domain W3C validator