Theorem isrng 20151

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

Hypotheses

Ref	Expression
isrng.b	⊢ 𝐵 = (Base‘𝑅)
isrng.g	⊢ 𝐺 = (mulGrp‘𝑅)
isrng.p	⊢ + = (+g‘𝑅)
isrng.t	⊢ · = (.r‘𝑅)

Assertion

Ref	Expression
isrng	⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ 𝐺 ∈ Smgrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))

Distinct variable groups:   𝑥,𝐵,𝑦,𝑧   𝑥,𝑅,𝑦,𝑧   𝑥, · ,𝑦,𝑧   𝑥, + ,𝑦,𝑧

Allowed substitution hints:   𝐺(𝑥,𝑦,𝑧)

Proof of Theorem isrng

Dummy variables 𝑏 𝑟 𝑡 𝑝 are mutually distinct and distinct from all other variables.

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ∀wral 3061  Vcvv 3480  [wsbc 3788  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  +_gcplusg 17297  ._rcmulr 17298  Smgrpcsgrp 18731  Abelcabl 19799  mulGrpcmgp 20137  Rngcrng 20149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-rng 20150

This theorem is referenced by:  rngabl  20152  rngmgp  20153  rngdi  20157  rngdir  20158  isrngd  20170  rngpropd  20171  prdsrngd  20173  ringrng  20282  isringrng  20284  rnglidlrng  21257  2zrngALT  48170  cznrng  48177