Theorem isring

Description: The predicate "is a (unital) ring". Definition of "ring with unit" in Schechter p. 187. (Contributed by NM, 18-Oct-2012) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	isring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isring.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	isring.p	⊢ + = ( +g ‘ 𝑅 )
	isring.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	isring	⊢ ( 𝑅 ∈ Ring ↔ ( 𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isring.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
3		isring.p	⊢ + = ( +g ‘ 𝑅 )
4		isring.t	⊢ · = ( .r ‘ 𝑅 )
5		fveq2	⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) )
6	5 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = 𝐺 )
7	6	eleq1d	⊢ ( 𝑟 = 𝑅 → ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ↔ 𝐺 ∈ Mnd ) )
8		fvexd	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) ∈ V )
9		fveq2	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
10	9 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
11		fvexd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑟 ) ∈ V )
12		simpl	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → 𝑟 = 𝑅 )
13	12	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑟 ) = ( +g ‘ 𝑅 ) )
14	13 3	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑟 ) = + )
15		fvexd	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → ( .r ‘ 𝑟 ) ∈ V )
16		simpll	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → 𝑟 = 𝑅 )
17	16	fveq2d	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
18	17 4	eqtr4di	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → ( .r ‘ 𝑟 ) = · )
19		simpllr	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑏 = 𝐵 )
20		simpr	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑡 = · )
21		eqidd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑥 = 𝑥 )
22		simplr	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑝 = + )
23	22	oveqd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑦 𝑝 𝑧 ) = ( 𝑦 + 𝑧 ) )
24	20 21 23	oveq123d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( 𝑥 · ( 𝑦 + 𝑧 ) ) )
25	20	oveqd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑥 𝑡 𝑦 ) = ( 𝑥 · 𝑦 ) )
26	20	oveqd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑥 𝑡 𝑧 ) = ( 𝑥 · 𝑧 ) )
27	22 25 26	oveq123d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
28	24 27	eqeq12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ↔ ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ) )
29	22	oveqd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑥 𝑝 𝑦 ) = ( 𝑥 + 𝑦 ) )
30		eqidd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑧 = 𝑧 )
31	20 29 30	oveq123d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 + 𝑦 ) · 𝑧 ) )
32	20	oveqd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑦 𝑡 𝑧 ) = ( 𝑦 · 𝑧 ) )
33	22 26 32	oveq123d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
34	31 33	eqeq12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ↔ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
35	28 34	anbi12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
36	19 35	raleqbidv	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
37	19 36	raleqbidv	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
38	19 37	raleqbidv	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
39	15 18 38	sbcied2	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → ( [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
40	11 14 39	sbcied2	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( [ ( +g ‘ 𝑟 ) / 𝑝 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
41	8 10 40	sbcied2	⊢ ( 𝑟 = 𝑅 → ( [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( +g ‘ 𝑟 ) / 𝑝 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
42	7 41	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ∧ [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( +g ‘ 𝑟 ) / 𝑝 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) )
43		df-ring	⊢ Ring = { 𝑟 ∈ Grp ∣ ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ∧ [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( +g ‘ 𝑟 ) / 𝑝 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) }
44	42 43	elrab2	⊢ ( 𝑅 ∈ Ring ↔ ( 𝑅 ∈ Grp ∧ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) )
45		3anass	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ↔ ( 𝑅 ∈ Grp ∧ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) )
46	44 45	bitr4i	⊢ ( 𝑅 ∈ Ring ↔ ( 𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )