Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rng0 Structured version   Unicode version

Definition df-rng0 39147
Description: Define class of all (non-unital) rings. A non-unital ring (or rng, or pseudoring) is a set equipped with two everywhere-defined internal operations, whose first one is an additive abelian group operation and the second one is a multiplicative semigroup operation, and where the addition is left- and right-distributive for the multiplication. Definition of a pseudo-ring in section I.8.1 of [BourbakiAlg1] p. 93 or the definition of a ring in part Preliminaries of [Roman] p. 18. As almost always in mathematics, "non-unital" means "not necessarily unital". Therefore, by talking about a ring (in general) or a non-unital ring the "unital" case is always included. In contrast to a unital ring, the commutativity of addition must be postulated and cannot be proven from the other conditions. (Contributed by AV, 6-Jan-2020.)
Assertion
Ref Expression
df-rng0  |- Rng  =  {
f  e.  Abel  |  ( (mulGrp `  f )  e. SGrp  /\  [. ( Base `  f )  /  b ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. A. x  e.  b  A. y  e.  b  A. z  e.  b 
( ( 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, b, p, t, x, y, z

Detailed syntax breakdown of Definition df-rng0
StepHypRef Expression
1 crng 39146 . 2  class Rng
2 vf . . . . . . 7  setvar  f
32cv 1436 . . . . . 6  class  f
4 cmgp 17711 . . . . . 6  class mulGrp
53, 4cfv 5598 . . . . 5  class  (mulGrp `  f )
6 csgrp 16514 . . . . 5  class SGrp
75, 6wcel 1868 . . . 4  wff  (mulGrp `  f )  e. SGrp
8 vx . . . . . . . . . . . . . 14  setvar  x
98cv 1436 . . . . . . . . . . . . 13  class  x
10 vy . . . . . . . . . . . . . . 15  setvar  y
1110cv 1436 . . . . . . . . . . . . . 14  class  y
12 vz . . . . . . . . . . . . . . 15  setvar  z
1312cv 1436 . . . . . . . . . . . . . 14  class  z
14 vp . . . . . . . . . . . . . . 15  setvar  p
1514cv 1436 . . . . . . . . . . . . . 14  class  p
1611, 13, 15co 6302 . . . . . . . . . . . . 13  class  ( y p z )
17 vt . . . . . . . . . . . . . 14  setvar  t
1817cv 1436 . . . . . . . . . . . . 13  class  t
199, 16, 18co 6302 . . . . . . . . . . . 12  class  ( x t ( y p z ) )
209, 11, 18co 6302 . . . . . . . . . . . . 13  class  ( x t y )
219, 13, 18co 6302 . . . . . . . . . . . . 13  class  ( x t z )
2220, 21, 15co 6302 . . . . . . . . . . . 12  class  ( ( x t y ) p ( x t z ) )
2319, 22wceq 1437 . . . . . . . . . . 11  wff  ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )
249, 11, 15co 6302 . . . . . . . . . . . . 13  class  ( x p y )
2524, 13, 18co 6302 . . . . . . . . . . . 12  class  ( ( x p y ) t z )
2611, 13, 18co 6302 . . . . . . . . . . . . 13  class  ( y t z )
2721, 26, 15co 6302 . . . . . . . . . . . 12  class  ( ( x t z ) p ( y t z ) )
2825, 27wceq 1437 . . . . . . . . . . 11  wff  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) )
2923, 28wa 370 . . . . . . . . . 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 vb . . . . . . . . . . 11  setvar  b
3130cv 1436 . . . . . . . . . 10  class  b
3229, 12, 31wral 2775 . . . . . . . . 9  wff  A. z  e.  b  ( (
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 2775 . . . . . . . 8  wff  A. y  e.  b  A. z  e.  b  ( (
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 2775 . . . . . . 7  wff  A. x  e.  b  A. y  e.  b  A. z  e.  b  ( (
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 15179 . . . . . . . 8  class  .r
363, 35cfv 5598 . . . . . . 7  class  ( .r
`  f )
3734, 17, 36wsbc 3299 . . . . . 6  wff  [. ( .r `  f )  / 
t ]. A. x  e.  b  A. y  e.  b  A. z  e.  b  ( ( 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 15178 . . . . . . 7  class  +g
393, 38cfv 5598 . . . . . 6  class  ( +g  `  f )
4037, 14, 39wsbc 3299 . . . . 5  wff  [. ( +g  `  f )  /  p ]. [. ( .r
`  f )  / 
t ]. A. x  e.  b  A. y  e.  b  A. z  e.  b  ( ( 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 15109 . . . . . 6  class  Base
423, 41cfv 5598 . . . . 5  class  ( Base `  f )
4340, 30, 42wsbc 3299 . . . 4  wff  [. ( Base `  f )  / 
b ]. [. ( +g  `  f )  /  p ]. [. ( .r `  f )  /  t ]. A. x  e.  b 
A. y  e.  b 
A. z  e.  b  ( ( 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 370 . . 3  wff  ( (mulGrp `  f )  e. SGrp  /\  [. ( Base `  f
)  /  b ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. A. x  e.  b  A. y  e.  b  A. z  e.  b 
( ( 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 cabl 17419 . . 3  class  Abel
4644, 2, 45crab 2779 . 2  class  { f  e.  Abel  |  (
(mulGrp `  f )  e. SGrp  /\  [. ( Base `  f )  /  b ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. A. x  e.  b  A. y  e.  b  A. z  e.  b 
( ( 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 1437 1  wff Rng  =  {
f  e.  Abel  |  ( (mulGrp `  f )  e. SGrp  /\  [. ( Base `  f )  /  b ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. A. x  e.  b  A. y  e.  b  A. z  e.  b 
( ( 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 setvar class
This definition is referenced by:  isrng  39148
  Copyright terms: Public domain W3C validator