Theorem primrootsunit1 42054

Description: Primitive roots have left inverses. (Contributed by metakunt, 25-Apr-2025.)

Hypotheses

Ref	Expression
primrootsunit1.1	⊢ (𝜑 → 𝑅 ∈ CMnd)
primrootsunit1.2	⊢ (𝜑 → 𝐾 ∈ ℕ)
primrootsunit1.3	⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}

Assertion

Ref	Expression
primrootsunit1	⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))

Distinct variable groups:   𝑖,𝐾   𝑅,𝑎,𝑖   𝑈,𝑖   𝜑,𝑖

Allowed substitution hints:   𝜑(𝑎)   𝑈(𝑎)   𝐾(𝑎)

Proof of Theorem primrootsunit1

Dummy variables 𝑐 𝑙 𝑏 𝑑 𝑗 𝑞 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		primrootsunit1.1	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑅 ∈ CMnd)
2	1	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
3		primrootsunit1.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ ℕ)
4	3	nnnn0d 12613	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
5	4	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℕ0)
6		eqid 2740	. . . . . . . . . . . . . . 15 ⊢ (.g‘𝑅) = (.g‘𝑅)
7	2, 5, 6	isprimroot 42050	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
8	7	biimpd 229	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
9	8	syldbl2 840	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
10	9	simp1d 1142	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ (Base‘𝑅))
11	1	cmnmndd 19846	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Mnd)
12	11	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ Mnd)
13		nnm1nn0 12594	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈ ℕ0)
14	3, 13	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐾 − 1) ∈ ℕ0)
15	14	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾 − 1) ∈ ℕ0)
16		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (Base‘𝑅) = (Base‘𝑅)
17	16, 6	mulgnn0cl 19130	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Mnd ∧ (𝐾 − 1) ∈ ℕ0 ∧ 𝑐 ∈ (Base‘𝑅)) → ((𝐾 − 1)(.g‘𝑅)𝑐) ∈ (Base‘𝑅))
18	12, 15, 10, 17	syl3anc 1371	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐾 − 1)(.g‘𝑅)𝑐) ∈ (Base‘𝑅))
19		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐))
20	19	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → (𝑖(+g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
21	20	eqeq1d 2742	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → ((𝑖(+g‘𝑅)𝑐) = (0g‘𝑅) ↔ (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (0g‘𝑅)))
22	3	nncnd 12309	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ ℂ)
23		1cnd 11285	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℂ)
24	22, 23	npcand 11651	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐾 − 1) + 1) = 𝐾)
25	24	eqcomd 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 = ((𝐾 − 1) + 1))
26	25	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 = ((𝐾 − 1) + 1))
27	26	oveq1d 7463	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (((𝐾 − 1) + 1)(.g‘𝑅)𝑐))
28		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (+g‘𝑅) = (+g‘𝑅)
29	16, 6, 28	mulgnn0p1 19125	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Mnd ∧ (𝐾 − 1) ∈ ℕ0 ∧ 𝑐 ∈ (Base‘𝑅)) → (((𝐾 − 1) + 1)(.g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
30	12, 15, 10, 29	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1) + 1)(.g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
31	27, 30	eqtr2d 2781	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (𝐾(.g‘𝑅)𝑐))
32	9	simp2d 1143	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅))
33	31, 32	eqtrd 2780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (0g‘𝑅))
34	18, 21, 33	rspcedvd 3637	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅))
35	10, 34	jca 511	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
36		oveq2 7456	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑐))
37	36	eqeq1d 2742	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
38	37	rexbidv 3185	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
39	38	elrab 3708	. . . . . . . . . 10 ⊢ (𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑐 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
40	35, 39	sylibr 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
41		primrootsunit1.3	. . . . . . . . . 10 ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}
42	41	eleq2i 2836	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
43	40, 42	sylibr 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ 𝑈)
44		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝜑)
45	41	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
46	45	eleq2d 2830	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
47	46	biimpd 229	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑏 ∈ 𝑈 → 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
48	47	imp 406	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
49	44, 48	jca 511	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (𝜑 ∧ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
50		elrabi 3703	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑏 ∈ (Base‘𝑅))
51	50	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}) → 𝑏 ∈ (Base‘𝑅))
52	49, 51	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
53	52	ex 412	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑏 ∈ 𝑈 → 𝑏 ∈ (Base‘𝑅)))
54	53	ssrdv 4014	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑅))
55		eqid 2740	. . . . . . . . . . . 12 ⊢ (𝑅 ↾s 𝑈) = (𝑅 ↾s 𝑈)
56	55, 16	ressbas2 17296	. . . . . . . . . . 11 ⊢ (𝑈 ⊆ (Base‘𝑅) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
57	54, 56	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
58	57	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
59	58	eleq2d 2830	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
60	43, 59	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)))
61	11	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑅 ∈ Mnd)
62	52	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
63		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝜑)
64	45	eleq2d 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
65	64	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝑑 ∈ 𝑈 → 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
66	65	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
67	63, 66	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → (𝜑 ∧ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
68		elrabi 3703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑑 ∈ (Base‘𝑅))
69	68	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}) → 𝑑 ∈ (Base‘𝑅))
70	67, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
71	44, 70	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
72	16, 28	mndcl 18780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ Mnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))
73	61, 62, 71, 72	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))
74	41	eleq2i 2836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
75		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑎 = 𝑑 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑑))
76	75	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑎 = 𝑑 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
77	76	rexbidv 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 = 𝑑 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
78	77	elrab 3708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
79	74, 78	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑑 ∈ 𝑈 ↔ (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
80	79	biimpi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑑 ∈ 𝑈 → (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
81	80	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑑 ∈ 𝑈 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
82	81	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
83	1	ad4antr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑅 ∈ CMnd)
84	71	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑑 ∈ (Base‘𝑅))
85		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑖 ∈ (Base‘𝑅))
86	16, 28	cmncom 19840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑅 ∈ CMnd ∧ 𝑑 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑑))
87	83, 84, 85, 86	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑑))
88		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
89	87, 88	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (0g‘𝑅))
90	89	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) → ((𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → (𝑑(+g‘𝑅)𝑖) = (0g‘𝑅)))
91	90	reximdva 3174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → ∃𝑖 ∈ (Base‘𝑅)(𝑑(+g‘𝑅)𝑖) = (0g‘𝑅)))
92	82, 91	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑑(+g‘𝑅)𝑖) = (0g‘𝑅))
93	16, 61, 71, 92	mndmolinv 42052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
94	82, 93	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
95		reu5 3390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ↔ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
96	94, 95	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
97		riotacl 7422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅))
99		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (0g‘𝑅) = (0g‘𝑅)
100		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (invg‘𝑅) = (invg‘𝑅)
101	16, 28, 99, 100	grpinvval 19020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑑 ∈ (Base‘𝑅) → ((invg‘𝑅)‘𝑑) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
102	71, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑑) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
103	102	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ↔ (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅)))
104	98, 103	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅))
105	41	eleq2i 2836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
106		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑎 = 𝑏 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑏))
107	106	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑎 = 𝑏 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
108	107	rexbidv 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 = 𝑏 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
109	108	elrab 3708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
110	105, 109	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑏 ∈ 𝑈 ↔ (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
111	110	biimpi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑏 ∈ 𝑈 → (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
112	111	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑏 ∈ 𝑈 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
113	112	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
114	1	ad4antr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑅 ∈ CMnd)
115	62	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑏 ∈ (Base‘𝑅))
116		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑖 ∈ (Base‘𝑅))
117	16, 28	cmncom 19840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑅 ∈ CMnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑏))
118	114, 115, 116, 117	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑏))
119		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
120	118, 119	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (0g‘𝑅))
121	120	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) → ((𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → (𝑏(+g‘𝑅)𝑖) = (0g‘𝑅)))
122	121	reximdva 3174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → ∃𝑖 ∈ (Base‘𝑅)(𝑏(+g‘𝑅)𝑖) = (0g‘𝑅)))
123	113, 122	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑏(+g‘𝑅)𝑖) = (0g‘𝑅))
124	16, 61, 62, 123	mndmolinv 42052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
125	113, 124	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
126		reu5 3390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ↔ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
127	125, 126	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
128		riotacl 7422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅))
129	127, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅))
130	16, 28, 99, 100	grpinvval 19020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑏 ∈ (Base‘𝑅) → ((invg‘𝑅)‘𝑏) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
131	62, 130	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑏) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
132	131	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ↔ (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅)))
133	129, 132	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅))
134	16, 28	mndcl 18780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑅 ∈ Mnd ∧ ((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅)) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) ∈ (Base‘𝑅))
135	61, 104, 133, 134	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) ∈ (Base‘𝑅))
136		oveq1 7455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) → (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
137	136	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) → ((𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅) ↔ ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
138	137	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))) → ((𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅) ↔ ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
139	104, 133, 73	3jca 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅)))
140	16, 28	mndass 18781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))))
141	61, 139, 140	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))))
142	133, 62, 71	3jca 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)))
143	16, 28	mndass 18781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅))) → ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑) = (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
144	143	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅))) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑))
145	61, 142, 144	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑))
146	145	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)))
147	62, 127	linvh 42053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏) = (0g‘𝑅))
148	147	oveq1d 7463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑) = ((0g‘𝑅)(+g‘𝑅)𝑑))
149	148	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)))
150	16, 28, 99	mndlid 18792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑅 ∈ Mnd ∧ 𝑑 ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)𝑑) = 𝑑)
151	61, 71, 150	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((0g‘𝑅)(+g‘𝑅)𝑑) = 𝑑)
152	151	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)𝑑))
153	71, 96	linvh 42053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)𝑑) = (0g‘𝑅))
154	152, 153	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)) = (0g‘𝑅))
155	149, 154	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)) = (0g‘𝑅))
156	146, 155	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))) = (0g‘𝑅))
157	141, 156	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅))
158	135, 138, 157	rspcedvd 3637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅))
159	73, 158	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
160		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
161	160	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
162	161	rexbidv 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
163	162	elrab 3708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ ((𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
164	159, 163	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
165	41	eleq2i 2836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
166	165	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
167	164, 166	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
168	167	ralrimiva 3152	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
169	168	ralrimiva 3152	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
170		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = (0g‘𝑅) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(0g‘𝑅)))
171	170	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 = (0g‘𝑅) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
172	171	rexbidv 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (0g‘𝑅) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
173	16, 99	mndidcl 18787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑅 ∈ Mnd → (0g‘𝑅) ∈ (Base‘𝑅))
174	11, 173	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅))
175	11, 174	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)))
176	16, 28, 99	mndlid 18792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
177	175, 176	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
178	174, 177	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((0g‘𝑅) ∈ (Base‘𝑅) ∧ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
179		oveq1 7455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (0g‘𝑅) → (𝑖(+g‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)))
180	179	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = (0g‘𝑅) → ((𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅) ↔ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
181	180	rspcev 3635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((0g‘𝑅) ∈ (Base‘𝑅) ∧ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
182	178, 181	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
183	172, 174, 182	elrabd 3710	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
184	45	eleq2d 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((0g‘𝑅) ∈ 𝑈 ↔ (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
185	183, 184	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (0g‘𝑅) ∈ 𝑈)
186	16, 28, 99, 55	issubmnd 18799	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ Mnd ∧ 𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈) → ((𝑅 ↾s 𝑈) ∈ Mnd ↔ ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈))
187	11, 54, 185, 186	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Mnd ↔ ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈))
188	169, 187	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd)
189	45	eleq2d 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝑞 ∈ 𝑈 ↔ 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
190	189	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (𝑞 ∈ 𝑈 → 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
191	190	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
192		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑎 = 𝑞 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑞))
193	192	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑞 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
194	193	rexbidv 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑞 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
195	194	elrab 3708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑞 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
196	191, 195	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (𝑞 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
197	196	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
198		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑖 ∈ (Base‘𝑅))
199	196	simpld 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → 𝑞 ∈ (Base‘𝑅))
200	199	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑞 ∈ (Base‘𝑅))
201		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → 𝑗 = 𝑞)
202	201	oveq1d 7463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → (𝑗(+g‘𝑅)𝑖) = (𝑞(+g‘𝑅)𝑖))
203	202	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → ((𝑗(+g‘𝑅)𝑖) = (0g‘𝑅) ↔ (𝑞(+g‘𝑅)𝑖) = (0g‘𝑅)))
204	1	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑅 ∈ CMnd)
205	16, 28	cmncom 19840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ CMnd ∧ 𝑖 ∈ (Base‘𝑅) ∧ 𝑞 ∈ (Base‘𝑅)) → (𝑖(+g‘𝑅)𝑞) = (𝑞(+g‘𝑅)𝑖))
206	204, 198, 200, 205	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖(+g‘𝑅)𝑞) = (𝑞(+g‘𝑅)𝑖))
207		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
208	206, 207	eqtr3d 2782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑞(+g‘𝑅)𝑖) = (0g‘𝑅))
209	200, 203, 208	rspcedvd 3637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅))
210	198, 209	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
211		nfv 1913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Ⅎ𝑗(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)
212		nfv 1913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Ⅎ𝑖(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)
213		oveq1 7455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑖 = 𝑗 → (𝑖(+g‘𝑅)𝑎) = (𝑗(+g‘𝑅)𝑎))
214	213	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑖 = 𝑗 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)))
215	211, 212, 214	cbvrexw 3313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅))
216	215	rabbii 3449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)}
217	41, 216	eqtri 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)}
218	217	eleq2i 2836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 ∈ 𝑈 ↔ 𝑖 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)})
219		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑎 = 𝑖 → (𝑗(+g‘𝑅)𝑎) = (𝑗(+g‘𝑅)𝑖))
220	219	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑖 → ((𝑗(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
221	220	rexbidv 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑖 → (∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
222	221	elrab 3708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
223	218, 222	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ 𝑈 ↔ (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
224	210, 223	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑖 ∈ 𝑈)
225	197, 224, 207	reximssdv 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑖 ∈ 𝑈 (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
226		fvexd 6935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (Base‘𝑅) ∈ V)
227	41, 226	rabexd 5358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → 𝑈 ∈ V)
228	55, 28	ressplusg 17349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑈 ∈ V → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
229	227, 228	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
230	229	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
231	230	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
232	231	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
233		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑤 = 𝑖)
234		eqidd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑞 = 𝑞)
235	232, 233, 234	oveq123d 7469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (𝑖(+g‘𝑅)𝑞))
236	55, 16, 99	ress0g 18800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝑅)) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
237	11, 185, 54, 236	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
238	237	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
239	238	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
240	239	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
241	235, 240	eqeq12d 2756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → ((𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
242		eqidd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑈 = 𝑈)
243	241, 242	cbvrexdva2 3357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (∃𝑤 ∈ 𝑈 (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)) ↔ ∃𝑖 ∈ 𝑈 (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
244	225, 243	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
245	57	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (Base‘(𝑅 ↾s 𝑈)) = 𝑈)
246	245	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (Base‘(𝑅 ↾s 𝑈)) = 𝑈)
247	244, 246	rexeqtrrdv 3339	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
248	247	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑞 ∈ 𝑈 → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
249	57	eleq2d 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑞 ∈ 𝑈 ↔ 𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))))
250	249	imbi1d 341	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝑞 ∈ 𝑈 → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))) ↔ (𝑞 ∈ (Base‘(𝑅 ↾s 𝑈)) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))))
251	248, 250	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑞 ∈ (Base‘(𝑅 ↾s 𝑈)) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
252	251	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
253	252	ralrimiva 3152	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
254	188, 253	jca 511	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Mnd ∧ ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
255		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Base‘(𝑅 ↾s 𝑈)) = (Base‘(𝑅 ↾s 𝑈))
256		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+g‘(𝑅 ↾s 𝑈)) = (+g‘(𝑅 ↾s 𝑈))
257		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0g‘(𝑅 ↾s 𝑈)) = (0g‘(𝑅 ↾s 𝑈))
258	255, 256, 257	isgrp 18979	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ↾s 𝑈) ∈ Grp ↔ ((𝑅 ↾s 𝑈) ∈ Mnd ∧ ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
259	254, 258	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Grp)
260	259	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑅 ↾s 𝑈) ∈ Grp)
261		simplr 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ 𝑈)
262	57	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
263	262	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
264	263	eleq2d 2830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈))))
265	261, 264	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈)))
266		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ 𝑈)
267	263	eleq2d 2830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈))))
268	266, 267	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈)))
269	255, 256	grpcl 18981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈))) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈)))
270	260, 265, 268, 269	syl3anc 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈)))
271	263	eleq2d 2830	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈 ↔ (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈))))
272	270, 271	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈)
273	229	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
274	273	oveqdr 7476	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) = (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑))
275	274	eleq1d 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈))
276	272, 275	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
277	276	ralrimiva 3152	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
278	277	ralrimiva 3152	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
279	278, 187	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd)
280	11, 279	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd))
281	54, 185	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈))
282	280, 281	jca 511	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
283	16, 99	issubmndb 18840	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (SubMnd‘𝑅) ↔ ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
284	282, 283	sylibr 234	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ (SubMnd‘𝑅))
285	284	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
286	285, 5, 43	3jca 1128	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈))
287		eqid 2740	. . . . . . . . . . . 12 ⊢ (.g‘(𝑅 ↾s 𝑈)) = (.g‘(𝑅 ↾s 𝑈))
288	6, 55, 287	submmulg 19158	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝐾(.g‘𝑅)𝑐) = (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐))
289	288	eqcomd 2746	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝐾(.g‘𝑅)𝑐))
290	286, 289	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝐾(.g‘𝑅)𝑐))
291	238	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
292	290, 291	eqeq12d 2756	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅)))
293	32, 292	mpbird 257	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)))
294	9	simp3d 1144	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))
295		eqidd 2741	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ℕ0 = ℕ0)
296	285	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑈 ∈ (SubMnd‘𝑅))
297		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑙 ∈ ℕ0)
298	43	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑐 ∈ 𝑈)
299	296, 297, 298	3jca 1128	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑈 ∈ (SubMnd‘𝑅) ∧ 𝑙 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈))
300	6, 55, 287	submmulg 19158	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝑙 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
301	299, 300	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
302	237	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
303	301, 302	eqeq12d 2756	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) ↔ (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈))))
304	303	imbi1d 341	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
305	295, 304	raleqbidva 3340	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
306	294, 305	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))
307	60, 293, 306	3jca 1128	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
308	1	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑅 ∈ CMnd)
309	62	3impa 1110	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
310	71	3impa 1110	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
311	16, 28	cmncom 19840	. . . . . . . . . 10 ⊢ ((𝑅 ∈ CMnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑑) = (𝑑(+g‘𝑅)𝑏))
312	308, 309, 310, 311	syl3anc 1371	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) = (𝑑(+g‘𝑅)𝑏))
313	57, 229, 279, 312	iscmnd 19836	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ CMnd)
314	313, 4, 287	isprimroot 42050	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
315	314	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
316	307, 315	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
317	316	ex 412	. . . 4 ⊢ (𝜑 → (𝑐 ∈ (𝑅 PrimRoots 𝐾) → 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
318	317	ssrdv 4014	. . 3 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
319	313	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ CMnd)
320	4	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐾 ∈ ℕ0)
321	319, 320, 287	isprimroot 42050	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
322	321	biimpd 229	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
323	322	syldbl2 840	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
324	323	simp1d 1142	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)))
325	54	sselda 4008	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑈) → 𝑐 ∈ (Base‘𝑅))
326	325	ex 412	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑐 ∈ 𝑈 → 𝑐 ∈ (Base‘𝑅)))
327	57	eleq2d 2830	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
328	327	imbi1d 341	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑐 ∈ 𝑈 → 𝑐 ∈ (Base‘𝑅)) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅))))
329	326, 328	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅)))
330	329	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅)))
331	330	imp 406	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))) → 𝑐 ∈ (Base‘𝑅))
332	324, 331	mpdan 686	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (Base‘𝑅))
333	284	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
334	327	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
335	324, 334	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ 𝑈)
336	333, 320, 335, 288	syl3anc 1371	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐))
337	323	simp2d 1143	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)))
338	238	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
339	336, 337, 338	3eqtrd 2784	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅))
340	323	simp3d 1144	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))
341	333	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑈 ∈ (SubMnd‘𝑅))
342		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑙 ∈ ℕ0)
343	335	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑐 ∈ 𝑈)
344	341, 342, 343, 300	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
345	344	eqcomd 2746	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝑙(.g‘𝑅)𝑐))
346	338	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
347	345, 346	eqeq12d 2756	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝑙(.g‘𝑅)𝑐) = (0g‘𝑅)))
348	347	imbi1d 341	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙) ↔ ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
349	348	ralbidva 3182	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
350	340, 349	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))
351	332, 339, 350	3jca 1128	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
352	1	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
353	352, 320, 6	isprimroot 42050	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
354	351, 353	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (𝑅 PrimRoots 𝐾))
355	354	ex 412	. . . 4 ⊢ (𝜑 → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → 𝑐 ∈ (𝑅 PrimRoots 𝐾)))
356	355	ssrdv 4014	. . 3 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ (𝑅 PrimRoots 𝐾))
357	318, 356	eqssd 4026	. 2 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
358	259, 313	jca 511	. . 3 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑅 ↾s 𝑈) ∈ CMnd))
359		isabl 19826	. . 3 ⊢ ((𝑅 ↾s 𝑈) ∈ Abel ↔ ((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑅 ↾s 𝑈) ∈ CMnd))
360	358, 359	sylibr 234	. 2 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Abel)
361	357, 360	jca 511	1 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ∃wrex 3076  ∃!wreu 3386  ∃*wrmo 3387  {crab 3443  Vcvv 3488   ⊆ wss 3976   class class class wbr 5166  ‘cfv 6573  ℩crio 7403  (class class class)co 7448  1c1 11185   + caddc 11187   − cmin 11520  ℕcn 12293  ℕ₀cn0 12553   ∥ cdvds 16302  Basecbs 17258   ↾_s cress 17287  +_gcplusg 17311  0_gc0g 17499  Mndcmnd 18772  SubMndcsubmnd 18817  Grpcgrp 18973  inv_gcminusg 18974  ._gcmg 19107  CMndccmn 19822  Abelcabl 19823   PrimRoots cprimroots 42048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-2 12356  df-n0 12554  df-z 12640  df-uz 12904  df-fz 13568  df-seq 14053  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-0g 17501  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-submnd 18819  df-grp 18976  df-minusg 18977  df-mulg 19108  df-cmn 19824  df-abl 19825  df-primroots 42049

This theorem is referenced by:  primrootsunit  42055