Theorem isrng

Description: The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020)

	Ref	Expression
Hypotheses	isrng.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isrng.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	isrng.p	⊢ + = ( +g ‘ 𝑅 )
	isrng.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	isrng	⊢ ( 𝑅 ∈ Rng ↔ ( 𝑅 ∈ Abel ∧ 𝐺 ∈ Smgrp ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )

Proof

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