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 = { 𝑓 ∈ Abel ∣ ( ( mulGrp ‘ 𝑓 ) ∈ Smgrp ∧ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crng	⊢ Rng
1		vf	⊢ 𝑓
2		cabl	⊢ Abel
3		cmgp	⊢ mulGrp
4	1	cv	⊢ 𝑓
5	4 3	cfv	⊢ ( mulGrp ‘ 𝑓 )
6		csgrp	⊢ Smgrp
7	5 6	wcel	⊢ ( mulGrp ‘ 𝑓 ) ∈ Smgrp
8		cbs	⊢ Base
9	4 8	cfv	⊢ ( Base ‘ 𝑓 )
10		vb	⊢ 𝑏
11		cplusg	⊢ +g
12	4 11	cfv	⊢ ( +g ‘ 𝑓 )
13		vp	⊢ 𝑝
14		cmulr	⊢ .r
15	4 14	cfv	⊢ ( .r ‘ 𝑓 )
16		vt	⊢ 𝑡
17		vx	⊢ 𝑥
18	10	cv	⊢ 𝑏
19		vy	⊢ 𝑦
20		vz	⊢ 𝑧
21	17	cv	⊢ 𝑥
22	16	cv	⊢ 𝑡
23	19	cv	⊢ 𝑦
24	13	cv	⊢ 𝑝
25	20	cv	⊢ 𝑧
26	23 25 24	co	⊢ ( 𝑦 𝑝 𝑧 )
27	21 26 22	co	⊢ ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) )
28	21 23 22	co	⊢ ( 𝑥 𝑡 𝑦 )
29	21 25 22	co	⊢ ( 𝑥 𝑡 𝑧 )
30	28 29 24	co	⊢ ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) )
31	27 30	wceq	⊢ ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) )
32	21 23 24	co	⊢ ( 𝑥 𝑝 𝑦 )
33	32 25 22	co	⊢ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 )
34	23 25 22	co	⊢ ( 𝑦 𝑡 𝑧 )
35	29 34 24	co	⊢ ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) )
36	33 35	wceq	⊢ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) )
37	31 36	wa	⊢ ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
38	37 20 18	wral	⊢ ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
39	38 19 18	wral	⊢ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
40	39 17 18	wral	⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
41	40 16 15	wsbc	⊢ [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
42	41 13 12	wsbc	⊢ [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
43	42 10 9	wsbc	⊢ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
44	7 43	wa	⊢ ( ( mulGrp ‘ 𝑓 ) ∈ Smgrp ∧ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) )
45	44 1 2	crab	⊢ { 𝑓 ∈ Abel ∣ ( ( mulGrp ‘ 𝑓 ) ∈ Smgrp ∧ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) }
46	0 45	wceq	⊢ Rng = { 𝑓 ∈ Abel ∣ ( ( mulGrp ‘ 𝑓 ) ∈ Smgrp ∧ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) }