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	Could not format assertion : No typesetting found for |- 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 ) ) ) ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crng	$$class\mathrm{Rng}$$
1		vf	$$setvarf$$
2		cabl	$$class\mathrm{Abel}$$
3		cmgp	$$class\mathrm{mulGrp}$$
4	1	cv	$$setvarf$$
5	4 3	cfv	$$class{\mathrm{mulGrp}}_f$$
6		csgrp	Could not format Smgrp : No typesetting found for class Smgrp with typecode class
7	5 6	wcel	Could not format ( mulGrp ` f ) e. Smgrp : No typesetting found for wff ( mulGrp ` f ) e. Smgrp with typecode wff
8		cbs	$$class\mathrm{Base}$$
9	4 8	cfv	$$class{\mathrm{Base}}_f$$
10		vb	$$setvarb$$
11		cplusg	$$class{+}_{𝑔}$$
12	4 11	cfv	$$class{+}_f$$
13		vp	$$setvarp$$
14		cmulr	$$class{\cdot }_{𝑟}$$
15	4 14	cfv	$$class{\cdot }_f$$
16		vt	$$setvart$$
17		vx	$$setvarx$$
18	10	cv	$$setvarb$$
19		vy	$$setvary$$
20		vz	$$setvarz$$
21	17	cv	$$setvarx$$
22	16	cv	$$setvart$$
23	19	cv	$$setvary$$
24	13	cv	$$setvarp$$
25	20	cv	$$setvarz$$
26	23 25 24	co	$$class\left(ypz\right)$$
27	21 26 22	co	$$class\left(xt\left(ypz\right)\right)$$
28	21 23 22	co	$$class\left(xty\right)$$
29	21 25 22	co	$$class\left(xtz\right)$$
30	28 29 24	co	$$class\left(\left(xty\right)p\left(xtz\right)\right)$$
31	27 30	wceq	$$wffxt\left(ypz\right)=\left(xty\right)p\left(xtz\right)$$
32	21 23 24	co	$$class\left(xpy\right)$$
33	32 25 22	co	$$class\left(\left(xpy\right)tz\right)$$
34	23 25 22	co	$$class\left(ytz\right)$$
35	29 34 24	co	$$class\left(\left(xtz\right)p\left(ytz\right)\right)$$
36	33 35	wceq	$$wff\left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)$$
37	31 36	wa	$$wff\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)$$
38	37 20 18	wral	$$wff\forall z\in b\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)$$
39	38 19 18	wral	$$wff\forall y\in b\forall z\in b\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)$$
40	39 17 18	wral	$$wff\forall x\in b\forall y\in b\forall z\in b\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)$$
41	40 16 15	wsbc	$$wff\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in b\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)$$
42	41 13 12	wsbc	$$wff\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in b\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)$$
43	42 10 9	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_f/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in b\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)$$
44	7 43	wa	Could not format ( ( 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 ) ) ) ) : No typesetting found for 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 ) ) ) ) with typecode wff
45	44 1 2	crab	Could not format { 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 ) ) ) ) } : No typesetting found for 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 ) ) ) ) } with typecode class
46	0 45	wceq	Could not format 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 ) ) ) ) } : No typesetting found for 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 ) ) ) ) } with typecode wff