Theorem issrg 13336

Description: The predicate "is a semiring". (Contributed by Thierry Arnoux, 21-Mar-2018.)

Hypotheses

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

Assertion

Ref	Expression
issrg	⊢ (𝑅 ∈ SRing ↔ (𝑅 ∈ CMnd ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 ))))

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

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

Proof of Theorem issrg

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

Step	Hyp	Ref	Expression
1		elex 2763	. 2 ⊢ (𝑅 ∈ SRing → 𝑅 ∈ V)
2		simp1 999	. . 3 ⊢ ((𝑅 ∈ CMnd ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 ))) → 𝑅 ∈ CMnd)
3	2	elexd 2765	. 2 ⊢ ((𝑅 ∈ CMnd ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 ))) → 𝑅 ∈ V)
4		issrg.g	. . . . . . . 8 ⊢ 𝐺 = (mulGrp‘𝑅)
5	4	eleq1i 2255	. . . . . . 7 ⊢ (𝐺 ∈ Mnd ↔ (mulGrp‘𝑅) ∈ Mnd)
6	5	bicomi 132	. . . . . 6 ⊢ ((mulGrp‘𝑅) ∈ Mnd ↔ 𝐺 ∈ Mnd)
7	6	a1i 9	. . . . 5 ⊢ (𝑅 ∈ V → ((mulGrp‘𝑅) ∈ Mnd ↔ 𝐺 ∈ Mnd))
8		issrg.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑅)
9		basfn 12573	. . . . . . . 8 ⊢ Base Fn V
10		funfvex 5551	. . . . . . . . 9 ⊢ ((Fun Base ∧ 𝑅 ∈ dom Base) → (Base‘𝑅) ∈ V)
11	10	funfni 5335	. . . . . . . 8 ⊢ ((Base Fn V ∧ 𝑅 ∈ V) → (Base‘𝑅) ∈ V)
12	9, 11	mpan 424	. . . . . . 7 ⊢ (𝑅 ∈ V → (Base‘𝑅) ∈ V)
13	8, 12	eqeltrid 2276	. . . . . 6 ⊢ (𝑅 ∈ V → 𝐵 ∈ V)
14		issrg.p	. . . . . . . . 9 ⊢ + = (+g‘𝑅)
15		plusgslid 12627	. . . . . . . . . 10 ⊢ (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ)
16	15	slotex 12542	. . . . . . . . 9 ⊢ (𝑅 ∈ V → (+g‘𝑅) ∈ V)
17	14, 16	eqeltrid 2276	. . . . . . . 8 ⊢ (𝑅 ∈ V → + ∈ V)
18	17	adantr 276	. . . . . . 7 ⊢ ((𝑅 ∈ V ∧ 𝑏 = 𝐵) → + ∈ V)
19		issrg.t	. . . . . . . . . 10 ⊢ · = (.r‘𝑅)
20		mulrslid 12646	. . . . . . . . . . 11 ⊢ (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ)
21	20	slotex 12542	. . . . . . . . . 10 ⊢ (𝑅 ∈ V → (.r‘𝑅) ∈ V)
22	19, 21	eqeltrid 2276	. . . . . . . . 9 ⊢ (𝑅 ∈ V → · ∈ V)
23	22	ad2antrr 488	. . . . . . . 8 ⊢ (((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) → · ∈ V)
24		issrg.0	. . . . . . . . . . 11 ⊢ 0 = (0g‘𝑅)
25		fn0g 12854	. . . . . . . . . . . 12 ⊢ 0g Fn V
26		funfvex 5551	. . . . . . . . . . . . 13 ⊢ ((Fun 0g ∧ 𝑅 ∈ dom 0g) → (0g‘𝑅) ∈ V)
27	26	funfni 5335	. . . . . . . . . . . 12 ⊢ ((0g Fn V ∧ 𝑅 ∈ V) → (0g‘𝑅) ∈ V)
28	25, 27	mpan 424	. . . . . . . . . . 11 ⊢ (𝑅 ∈ V → (0g‘𝑅) ∈ V)
29	24, 28	eqeltrid 2276	. . . . . . . . . 10 ⊢ (𝑅 ∈ V → 0 ∈ V)
30	29	ad3antrrr 492	. . . . . . . . 9 ⊢ ((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 0 ∈ V)
31		simp-4r 542	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → 𝑏 = 𝐵)
32		simplr 528	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → 𝑡 = · )
33		eqidd 2190	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → 𝑥 = 𝑥)
34		simpllr 534	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → 𝑝 = + )
35	34	oveqd 5914	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (𝑦𝑝𝑧) = (𝑦 + 𝑧))
36	32, 33, 35	oveq123d 5918	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (𝑥𝑡(𝑦𝑝𝑧)) = (𝑥 · (𝑦 + 𝑧)))
37	32	oveqd 5914	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (𝑥𝑡𝑦) = (𝑥 · 𝑦))
38	32	oveqd 5914	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (𝑥𝑡𝑧) = (𝑥 · 𝑧))
39	34, 37, 38	oveq123d 5918	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
40	36, 39	eqeq12d 2204	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ↔ (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))))
41	34	oveqd 5914	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (𝑥𝑝𝑦) = (𝑥 + 𝑦))
42		eqidd 2190	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → 𝑧 = 𝑧)
43	32, 41, 42	oveq123d 5918	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥 + 𝑦) · 𝑧))
44	32	oveqd 5914	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (𝑦𝑡𝑧) = (𝑦 · 𝑧))
45	34, 38, 44	oveq123d 5918	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
46	43, 45	eqeq12d 2204	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) ↔ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))
47	40, 46	anbi12d 473	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
48	31, 47	raleqbidv 2698	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
49	31, 48	raleqbidv 2698	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
50		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → 𝑛 = 0 )
51	32, 50, 33	oveq123d 5918	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (𝑛𝑡𝑥) = ( 0 · 𝑥))
52	51, 50	eqeq12d 2204	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ((𝑛𝑡𝑥) = 𝑛 ↔ ( 0 · 𝑥) = 0 ))
53	32, 33, 50	oveq123d 5918	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (𝑥𝑡𝑛) = (𝑥 · 0 ))
54	53, 50	eqeq12d 2204	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ((𝑥𝑡𝑛) = 𝑛 ↔ (𝑥 · 0 ) = 0 ))
55	52, 54	anbi12d 473	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛) ↔ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 )))
56	49, 55	anbi12d 473	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ((∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) ↔ (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 ))))
57	31, 56	raleqbidv 2698	. . . . . . . . 9 ⊢ (((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → (∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) ↔ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 ))))
58	30, 57	sbcied 3014	. . . . . . . 8 ⊢ ((((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ([ 0 / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) ↔ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 ))))
59	23, 58	sbcied 3014	. . . . . . 7 ⊢ (((𝑅 ∈ V ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) → ([ · / 𝑡][ 0 / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) ↔ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 ))))
60	18, 59	sbcied 3014	. . . . . 6 ⊢ ((𝑅 ∈ V ∧ 𝑏 = 𝐵) → ([ + / 𝑝][ · / 𝑡][ 0 / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) ↔ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 ))))
61	13, 60	sbcied 3014	. . . . 5 ⊢ (𝑅 ∈ V → ([𝐵 / 𝑏][ + / 𝑝][ · / 𝑡][ 0 / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) ↔ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 ))))
62	7, 61	anbi12d 473	. . . 4 ⊢ (𝑅 ∈ V → (((mulGrp‘𝑅) ∈ Mnd ∧ [𝐵 / 𝑏][ + / 𝑝][ · / 𝑡][ 0 / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))) ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 )))))
63	62	anbi2d 464	. . 3 ⊢ (𝑅 ∈ V → ((𝑅 ∈ CMnd ∧ ((mulGrp‘𝑅) ∈ Mnd ∧ [𝐵 / 𝑏][ + / 𝑝][ · / 𝑡][ 0 / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))) ↔ (𝑅 ∈ CMnd ∧ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 ))))))
64		fveq2 5534	. . . . . 6 ⊢ (𝑟 = 𝑅 → (mulGrp‘𝑟) = (mulGrp‘𝑅))
65	64	eleq1d 2258	. . . . 5 ⊢ (𝑟 = 𝑅 → ((mulGrp‘𝑟) ∈ Mnd ↔ (mulGrp‘𝑅) ∈ Mnd))
66		fveq2 5534	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
67	66, 8	eqtr4di 2240	. . . . . 6 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
68		fveq2 5534	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (+g‘𝑟) = (+g‘𝑅))
69	68, 14	eqtr4di 2240	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (+g‘𝑟) = + )
70		fveq2 5534	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅))
71	70, 19	eqtr4di 2240	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · )
72		fveq2 5534	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅))
73	72, 24	eqtr4di 2240	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 )
74	73	sbceq1d 2982	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ([(0g‘𝑟) / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) ↔ [ 0 / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))))
75	71, 74	sbceqbid 2984	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ([(.r‘𝑟) / 𝑡][(0g‘𝑟) / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) ↔ [ · / 𝑡][ 0 / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))))
76	69, 75	sbceqbid 2984	. . . . . 6 ⊢ (𝑟 = 𝑅 → ([(+g‘𝑟) / 𝑝][(.r‘𝑟) / 𝑡][(0g‘𝑟) / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) ↔ [ + / 𝑝][ · / 𝑡][ 0 / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))))
77	67, 76	sbceqbid 2984	. . . . 5 ⊢ (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑏][(+g‘𝑟) / 𝑝][(.r‘𝑟) / 𝑡][(0g‘𝑟) / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)) ↔ [𝐵 / 𝑏][ + / 𝑝][ · / 𝑡][ 0 / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))))
78	65, 77	anbi12d 473	. . . 4 ⊢ (𝑟 = 𝑅 → (((mulGrp‘𝑟) ∈ Mnd ∧ [(Base‘𝑟) / 𝑏][(+g‘𝑟) / 𝑝][(.r‘𝑟) / 𝑡][(0g‘𝑟) / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))) ↔ ((mulGrp‘𝑅) ∈ Mnd ∧ [𝐵 / 𝑏][ + / 𝑝][ · / 𝑡][ 0 / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))))
79		df-srg 13335	. . . 4 ⊢ SRing = {𝑟 ∈ CMnd ∣ ((mulGrp‘𝑟) ∈ Mnd ∧ [(Base‘𝑟) / 𝑏][(+g‘𝑟) / 𝑝][(.r‘𝑟) / 𝑡][(0g‘𝑟) / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
80	78, 79	elrab2 2911	. . 3 ⊢ (𝑅 ∈ SRing ↔ (𝑅 ∈ CMnd ∧ ((mulGrp‘𝑅) ∈ Mnd ∧ [𝐵 / 𝑏][ + / 𝑝][ · / 𝑡][ 0 / 𝑛]∀𝑥 ∈ 𝑏 (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))))
81		3anass 984	. . 3 ⊢ ((𝑅 ∈ CMnd ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 ))) ↔ (𝑅 ∈ CMnd ∧ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 )))))
82	63, 80, 81	3bitr4g 223	. 2 ⊢ (𝑅 ∈ V → (𝑅 ∈ SRing ↔ (𝑅 ∈ CMnd ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 )))))
83	1, 3, 82	pm5.21nii 705	1 ⊢ (𝑅 ∈ SRing ↔ (𝑅 ∈ CMnd ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 ))))

Syntax hints:   ∧ wa 104   ↔ wb 105   ∧ w3a 980   = wceq 1364   ∈ wcel 2160  ∀wral 2468  Vcvv 2752  [wsbc 2977   Fn wfn 5230  ‘cfv 5235  (class class class)co 5897  Basecbs 12515  +_gcplusg 12592  ._rcmulr 12593  0_gc0g 12764  Mndcmnd 12892  CMndccmn 13240  mulGrpcmgp 13291  SRingcsrg 13334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-cnex 7933  ax-resscn 7934  ax-1re 7936  ax-addrcl 7939

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-rab 2477  df-v 2754  df-sbc 2978  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-br 4019  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-iota 5196  df-fun 5237  df-fn 5238  df-fv 5243  df-riota 5852  df-ov 5900  df-inn 8951  df-2 9009  df-3 9010  df-ndx 12518  df-slot 12519  df-base 12521  df-plusg 12605  df-mulr 12606  df-0g 12766  df-srg 13335

This theorem is referenced by:  srgcmn  13337  srgmgp  13339  srgdilem  13340  srgrz  13355  srglz  13356  ringsrg  13416