Metamath Proof Explorer

Definition df-rng0

Description: Define class of all (non-unital) rings. Anon-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)

Ref Expression
Assertion df-rng0 
|- Rng = { f e. Abel | ( ( mulGrp ` f ) e. Smgrp /\ [. ( 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 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 crng 
 |-  Rng
1 vf 
 |-  f
2 cabl 
 |-  Abel
3 cmgp 
 |-  mulGrp
4 1 cv 
 |-  f
5 4 3 cfv 
 |-  ( mulGrp ` f )
6 csgrp 
 |-  Smgrp
7 5 6 wcel 
 |-  ( mulGrp ` f ) e. Smgrp
8 cbs 
 |-  Base
9 4 8 cfv 
 |-  ( Base ` f )
10 vb 
 |-  b
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 
 |-  b
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. 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 ) ) )
39 38 19 18 wral 
 |-  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 ) ) )
40 39 17 18 wral 
 |-  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 40 16 15 wsbc 
 |-  [. ( .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 ) ) )
42 41 13 12 wsbc 
 |-  [. ( +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 ) ) )
43 42 10 9 wsbc 
 |-  [. ( 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 ) ) )
44 7 43 wa 
 |-  ( ( mulGrp ` f ) e. Smgrp /\ [. ( 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 44 1 2 crab 
 |-  { f e. Abel | ( ( mulGrp ` f ) e. Smgrp /\ [. ( 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 ) ) ) ) }
46 0 45 wceq 
 |-  Rng = { f e. Abel | ( ( mulGrp ` f ) e. Smgrp /\ [. ( 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 ) ) ) ) }