Definition df-rng 13489

Description: Define the 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-rng	|- 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 ) ) ) ) }

Distinct variable group:   f, b, p, t, x, y, z

Detailed syntax breakdown of Definition df-rng

Step	Hyp	Ref	Expression
1		crng 13488	. 2 class Rng
2		vf	. . . . . . 7 setvar f
3	2	cv 1363	. . . . . 6 class f
4		cmgp 13476	. . . . . 6 class mulGrp
5	3, 4	cfv 5258	. . . . 5 class (mulGrp ` f )
6		csgrp 13044	. . . . 5 class Smgrp
7	5, 6	wcel 2167	. . . 4 wff (mulGrp ` f ) e. Smgrp
8		vx	. . . . . . . . . . . . . 14 setvar x
9	8	cv 1363	. . . . . . . . . . . . 13 class x
10		vy	. . . . . . . . . . . . . . 15 setvar y
11	10	cv 1363	. . . . . . . . . . . . . 14 class y
12		vz	. . . . . . . . . . . . . . 15 setvar z
13	12	cv 1363	. . . . . . . . . . . . . 14 class z
14		vp	. . . . . . . . . . . . . . 15 setvar p
15	14	cv 1363	. . . . . . . . . . . . . 14 class p
16	11, 13, 15	co 5922	. . . . . . . . . . . . 13 class ( y p z )
17		vt	. . . . . . . . . . . . . 14 setvar t
18	17	cv 1363	. . . . . . . . . . . . 13 class t
19	9, 16, 18	co 5922	. . . . . . . . . . . 12 class ( x t ( y p z ) )
20	9, 11, 18	co 5922	. . . . . . . . . . . . 13 class ( x t y )
21	9, 13, 18	co 5922	. . . . . . . . . . . . 13 class ( x t z )
22	20, 21, 15	co 5922	. . . . . . . . . . . 12 class ( ( x t y ) p ( x t z ) )
23	19, 22	wceq 1364	. . . . . . . . . . 11 wff ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) )
24	9, 11, 15	co 5922	. . . . . . . . . . . . 13 class ( x p y )
25	24, 13, 18	co 5922	. . . . . . . . . . . 12 class ( ( x p y ) t z )
26	11, 13, 18	co 5922	. . . . . . . . . . . . 13 class ( y t z )
27	21, 26, 15	co 5922	. . . . . . . . . . . 12 class ( ( x t z ) p ( y t z ) )
28	25, 27	wceq 1364	. . . . . . . . . . 11 wff ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) )
29	23, 28	wa 104	. . . . . . . . . 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
31	30	cv 1363	. . . . . . . . . 10 class b
32	29, 12, 31	wral 2475	. . . . . . . . 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 ) ) )
33	32, 10, 31	wral 2475	. . . . . . . 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 ) ) )
34	33, 8, 31	wral 2475	. . . . . . 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 12756	. . . . . . . 8 class .r
36	3, 35	cfv 5258	. . . . . . 7 class ( .r ` f )
37	34, 17, 36	wsbc 2989	. . . . . 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 12755	. . . . . . 7 class +g
39	3, 38	cfv 5258	. . . . . 6 class ( +g ` f )
40	37, 14, 39	wsbc 2989	. . . . 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 12678	. . . . . 6 class Base
42	3, 41	cfv 5258	. . . . 5 class ( Base ` f )
43	40, 30, 42	wsbc 2989	. . . 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 ) ) )
44	7, 43	wa 104	. . 3 wff ( (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		cabl 13415	. . 3 class Abel
46	44, 2, 45	crab 2479	. 2 class { 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 ) ) ) ) }
47	1, 46	wceq 1364	1 wff 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 ) ) ) ) }

This definition is referenced by:  isrng  13490