Metamath Proof Explorer

Definition df-ring

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. Definition 1 in BourbakiAlg1 p. 92 or definition of a ring with identity in part Preliminaries of Roman p. 19. So that the additive structure must be abelian (see ringcom ), 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. Therefore, it can be shown that a unital ring is a non-unital ring ( ringrng ) only after ringabl was proven. (Contributed by NM, 18-Oct-2012) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Assertion df-ring 
|- 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 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 crg 
 |-  Ring
1 vf 
 |-  f
2 cgrp 
 |-  Grp
3 cmgp 
 |-  mulGrp
4 1 cv 
 |-  f
5 4 3 cfv 
 |-  ( mulGrp ` f )
6 cmnd 
 |-  Mnd
7 5 6 wcel 
 |-  ( mulGrp ` f ) e. Mnd
8 cbs 
 |-  Base
9 4 8 cfv 
 |-  ( Base ` f )
10 vr 
 |-  r
11 cplusg 
 |-  +g
12 4 11 cfv 
 |-  ( +g ` f )
13 vp 
 |-  p
14 cmulr 
 |-  .r
15 4 14 cfv 
 |-  ( .r ` f )
16 vt 
 |-  t
17 vx 
 |-  x
18 10 cv 
 |-  r
19 vy 
 |-  y
20 vz 
 |-  z
21 17 cv 
 |-  x
22 16 cv 
 |-  t
23 19 cv 
 |-  y
24 13 cv 
 |-  p
25 20 cv 
 |-  z
26 23 25 24 co 
 |-  ( y p z )
27 21 26 22 co 
 |-  ( x t ( y p z ) )
28 21 23 22 co 
 |-  ( x t y )
29 21 25 22 co 
 |-  ( x t z )
30 28 29 24 co 
 |-  ( ( x t y ) p ( x t z ) )
31 27 30 wceq 
 |-  ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) )
32 21 23 24 co 
 |-  ( x p y )
33 32 25 22 co 
 |-  ( ( x p y ) t z )
34 23 25 22 co 
 |-  ( y t z )
35 29 34 24 co 
 |-  ( ( x t z ) p ( y t z ) )
36 33 35 wceq 
 |-  ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) )
37 31 36 wa 
 |-  ( ( 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 37 20 18 wral 
 |-  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 ) ) )
39 38 19 18 wral 
 |-  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 ) ) )
40 39 17 18 wral 
 |-  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 40 16 15 wsbc 
 |-  [. ( .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 ) ) )
42 41 13 12 wsbc 
 |-  [. ( +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 ) ) )
43 42 10 9 wsbc 
 |-  [. ( 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 ) ) )
44 7 43 wa 
 |-  ( ( 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 44 1 2 crab 
 |-  { 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 ) ) ) ) }
46 0 45 wceq 
 |-  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 ) ) ) ) }