Definition df-ring

Description: Define class of all (unital) rings. A unital ring is a set equipped with two everywhere-defined internal operations, whose first one is an additive group structure and the second one is a multiplicative monoid structure, and where the addition is left- and right-distributive for the multiplication. Definition 1 in BourbakiAlg1 p. 92 or definition of a ring with identity in part Preliminaries of Roman p. 19. So that the additive structure must be abelian (see ringcom ), care must be taken that in the case of a non-unital ring, the commutativity of addition must be postulated and cannot be proved from the other conditions. Therefore, it can be shown that a unital ring is a non-unital ring ( ringrng ) only after ringabl was proven. (Contributed by NM, 18-Oct-2012) (Revised by Mario Carneiro, 27-Dec-2014)

	Ref	Expression
Assertion	df-ring	⊢ Ring = { 𝑓 ∈ Grp ∣ ( ( mulGrp ‘ 𝑓 ) ∈ Mnd ∧ [ ( Base ‘ 𝑓 ) / 𝑟 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crg	⊢ Ring
1		vf	⊢ 𝑓
2		cgrp	⊢ Grp
3		cmgp	⊢ mulGrp
4	1	cv	⊢ 𝑓
5	4 3	cfv	⊢ ( mulGrp ‘ 𝑓 )
6		cmnd	⊢ Mnd
7	5 6	wcel	⊢ ( mulGrp ‘ 𝑓 ) ∈ Mnd
8		cbs	⊢ Base
9	4 8	cfv	⊢ ( Base ‘ 𝑓 )
10		vr	⊢ 𝑟
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 ‘ 𝑓 ) ∈ Mnd ∧ [ ( Base ‘ 𝑓 ) / 𝑟 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) )
45	44 1 2	crab	⊢ { 𝑓 ∈ Grp ∣ ( ( mulGrp ‘ 𝑓 ) ∈ Mnd ∧ [ ( Base ‘ 𝑓 ) / 𝑟 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) }
46	0 45	wceq	⊢ Ring = { 𝑓 ∈ Grp ∣ ( ( mulGrp ‘ 𝑓 ) ∈ Mnd ∧ [ ( Base ‘ 𝑓 ) / 𝑟 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) }