Theorem primrootscoprbij 42731

Description: A bijection between coprime powers of primitive roots and primitive roots. (Contributed by metakunt, 26-Apr-2025.)

Hypotheses

Ref	Expression
primrootscoprbij.1	⊢ 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚))
primrootscoprbij.2	⊢ (𝜑 → 𝑅 ∈ CMnd)
primrootscoprbij.3	⊢ (𝜑 → 𝐾 ∈ ℕ)
primrootscoprbij.4	⊢ (𝜑 → 𝐼 ∈ ℕ)
primrootscoprbij.5	⊢ (𝜑 → 𝐽 ∈ ℕ)
primrootscoprbij.6	⊢ (𝜑 → 𝑍 ∈ ℤ)
primrootscoprbij.7	⊢ (𝜑 → 1 = ((𝐼 · 𝐽) + (𝐾 · 𝑍)))
primrootscoprbij.8	⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}

Assertion

Ref	Expression
primrootscoprbij	⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)–1-1-onto→(𝑅 PrimRoots 𝐾))

Distinct variable groups:   𝑚,𝐼   𝑚,𝐽   𝑚,𝐾   𝑅,𝑎,𝑖   𝑅,𝑚   𝜑,𝑖   𝜑,𝑚

Allowed substitution hints:   𝜑(𝑎)   𝑈(𝑖,𝑚,𝑎)   𝐹(𝑖,𝑚,𝑎)   𝐼(𝑖,𝑎)   𝐽(𝑖,𝑎)   𝐾(𝑖,𝑎)   𝑍(𝑖,𝑚,𝑎)

Proof of Theorem primrootscoprbij

Dummy variables 𝑥 𝑦 𝑛 𝑙 𝑡 𝑓 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		primrootscoprbij.1	. . 3 ⊢ 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚))
2		primrootscoprbij.2	. . 3 ⊢ (𝜑 → 𝑅 ∈ CMnd)
3		primrootscoprbij.3	. . 3 ⊢ (𝜑 → 𝐾 ∈ ℕ)
4		primrootscoprbij.4	. . 3 ⊢ (𝜑 → 𝐼 ∈ ℕ)
5	4	nnzd 12608	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
6	3	nnzd 12608	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℤ)
7		primrootscoprbij.5	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℕ)
8	7	nnzd 12608	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ ℤ)
9		primrootscoprbij.6	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ ℤ)
10	8, 9	jca 520	. . . . . 6 ⊢ (𝜑 → (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ))
11	5, 6, 10	jca31 523	. . . . 5 ⊢ (𝜑 → ((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)))
12		primrootscoprbij.7	. . . . . 6 ⊢ (𝜑 → 1 = ((𝐼 · 𝐽) + (𝐾 · 𝑍)))
13	12	eqcomd 2771	. . . . 5 ⊢ (𝜑 → ((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1)
14	11, 13	jca 520	. . . 4 ⊢ (𝜑 → (((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1))
15		bezoutr1 16617	. . . . 5 ⊢ (((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)) → (((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1 → (𝐼 gcd 𝐾) = 1))
16	15	imp 411	. . . 4 ⊢ ((((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1) → (𝐼 gcd 𝐾) = 1)
17	14, 16	syl 18	. . 3 ⊢ (𝜑 → (𝐼 gcd 𝐾) = 1)
18	1, 2, 3, 4, 17	primrootscoprf 42730	. 2 ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)⟶(𝑅 PrimRoots 𝐾))
19		eqid 2765	. . 3 ⊢ (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)) = (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))
20	8, 6	jca 520	. . . . . 6 ⊢ (𝜑 → (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ))
21	5, 9	jca 520	. . . . . 6 ⊢ (𝜑 → (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ))
22	20, 21	jca 520	. . . . 5 ⊢ (𝜑 → ((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)))
23	7	nncnd 12240	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℂ)
24	4	nncnd 12240	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ ℂ)
25	23, 24	mulcomd 11218	. . . . . . 7 ⊢ (𝜑 → (𝐽 · 𝐼) = (𝐼 · 𝐽))
26	25	oveq1d 7415	. . . . . 6 ⊢ (𝜑 → ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = ((𝐼 · 𝐽) + (𝐾 · 𝑍)))
27	26, 13	eqtrd 2800	. . . . 5 ⊢ (𝜑 → ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1)
28	22, 27	jca 520	. . . 4 ⊢ (𝜑 → (((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1))
29		bezoutr1 16617	. . . . 5 ⊢ (((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)) → (((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1 → (𝐽 gcd 𝐾) = 1))
30	29	imp 411	. . . 4 ⊢ ((((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1) → (𝐽 gcd 𝐾) = 1)
31	28, 30	syl 18	. . 3 ⊢ (𝜑 → (𝐽 gcd 𝐾) = 1)
32	19, 2, 3, 7, 31	primrootscoprf 42730	. 2 ⊢ (𝜑 → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)):(𝑅 PrimRoots 𝐾)⟶(𝑅 PrimRoots 𝐾))
33	1	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚)))
34		simpr 489	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = 𝑥) → 𝑚 = 𝑥)
35	34	oveq2d 7416	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = 𝑥) → (𝐼(.g‘𝑅)𝑚) = (𝐼(.g‘𝑅)𝑥))
36		simpr 489	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑥 ∈ (𝑅 PrimRoots 𝐾))
37	2	cmnmndd 19865	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Mnd)
38	37	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ Mnd)
39	4	nnnn0d 12556	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ ℕ0)
40	39	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐼 ∈ ℕ0)
41	3	nnnn0d 12556	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
42		eqid 2765	. . . . . . . . . . 11 ⊢ (.g‘𝑅) = (.g‘𝑅)
43	2, 41, 42	isprimroot 42722	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
44	43	biimpd 232	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
45	44	imp 411	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
46	45	simp1d 1158	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑥 ∈ (Base‘𝑅))
47		eqid 2765	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
48	47, 42	mulgnn0cl 19147	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ ℕ0 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐼(.g‘𝑅)𝑥) ∈ (Base‘𝑅))
49	38, 40, 46, 48	syl3anc 1394	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)𝑥) ∈ (Base‘𝑅))
50	33, 35, 36, 49	fvmptd 6987	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘𝑥) = (𝐼(.g‘𝑅)𝑥))
51	50	fveq2d 6875	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)))
52		eqidd 2766	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)) = (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)))
53		simpr 489	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = (𝐼(.g‘𝑅)𝑥)) → 𝑛 = (𝐼(.g‘𝑅)𝑥))
54	53	oveq2d 7416	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = (𝐼(.g‘𝑅)𝑥)) → (𝐽(.g‘𝑅)𝑛) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
55	2	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
56	3	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℕ)
57	4	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐼 ∈ ℕ)
58	17	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 gcd 𝐾) = 1)
59		eqid 2765	. . . . . . 7 ⊢ {𝑠 ∈ (Base‘𝑅) ∣ ∃𝑡 ∈ (Base‘𝑅)(𝑡(+g‘𝑅)𝑠) = (0g‘𝑅)} = {𝑠 ∈ (Base‘𝑅) ∣ ∃𝑡 ∈ (Base‘𝑅)(𝑡(+g‘𝑅)𝑠) = (0g‘𝑅)}
60	55, 56, 57, 58, 36, 59	primrootscoprmpow 42728	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)𝑥) ∈ (𝑅 PrimRoots 𝐾))
61	7	nnnn0d 12556	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℕ0)
62	61	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐽 ∈ ℕ0)
63	47, 42	mulgnn0cl 19147	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐽 ∈ ℕ0 ∧ (𝐼(.g‘𝑅)𝑥) ∈ (Base‘𝑅)) → (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)) ∈ (Base‘𝑅))
64	38, 62, 49, 63	syl3anc 1394	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)) ∈ (Base‘𝑅))
65	52, 54, 60, 64	fvmptd 6987	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
66	62, 40, 46	3jca 1144	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝑥 ∈ (Base‘𝑅)))
67	47, 42	mulgnn0ass 19167	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ (𝐽 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝑥 ∈ (Base‘𝑅))) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
68	38, 66, 67	syl2anc 595	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
69		primrootscoprbij.8	. . . . . . . . . . . 12 ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}
70	2, 3, 69	primrootsunit 42727	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))
71	70	simpld 499	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
72	71	eleq2d 2851	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) ↔ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
73	72	biimpd 232	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) → 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
74	70	simprd 500	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Abel)
75		ablgrp 19846	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ↾s 𝑈) ∈ Abel → (𝑅 ↾s 𝑈) ∈ Grp)
76	74, 75	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Grp)
77		grpmnd 18997	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ↾s 𝑈) ∈ Grp → (𝑅 ↾s 𝑈) ∈ Mnd)
78	76, 77	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd)
79	37, 78	jca 520	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd))
80	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
81	80	eleq2d 2851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑓 ∈ 𝑈 ↔ 𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
82	81	biimpd 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑓 ∈ 𝑈 → 𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
83	82	imp 411	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑈) → 𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
84		oveq2 7408	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑓 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑓))
85	84	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑓 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
86	85	rexbidv 3189	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑓 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
87	86	elrab 3653	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑓 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
88	87	biimpi 219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → (𝑓 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
89	88	simpld 499	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑓 ∈ (Base‘𝑅))
90	83, 89	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑈) → 𝑓 ∈ (Base‘𝑅))
91	90	ex 417	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑓 ∈ 𝑈 → 𝑓 ∈ (Base‘𝑅)))
92	91	ssrdv 3945	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑅))
93		oveq2 7408	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (0g‘𝑅) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(0g‘𝑅)))
94	93	eqeq1d 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (0g‘𝑅) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
95	94	rexbidv 3189	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (0g‘𝑅) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
96		eqid 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0g‘𝑅) = (0g‘𝑅)
97	47, 96	mndidcl 18797	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ Mnd → (0g‘𝑅) ∈ (Base‘𝑅))
98	37, 97	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅))
99		simpr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → 𝑖 = (0g‘𝑅))
100	99	oveq1d 7415	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → (𝑖(+g‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)))
101	100	eqeq1d 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → ((𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅) ↔ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
102		eqid 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (+g‘𝑅) = (+g‘𝑅)
103	47, 102, 96	mndlid 18802	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
104	37, 98, 103	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
105	98, 101, 104	rspcedvd 3586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
106	95, 98, 105	elrabd 3655	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
107	80	eleq2d 2851	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0g‘𝑅) ∈ 𝑈 ↔ (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
108	106, 107	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0g‘𝑅) ∈ 𝑈)
109	92, 108	jca 520	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈))
110	79, 109	jca 520	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
111	47, 96	issubmndb 18853	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ (SubMnd‘𝑅) ↔ ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
112	110, 111	sylibr 237	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ (SubMnd‘𝑅))
113	112	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
114	61	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐽 ∈ ℕ0)
115	39	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐼 ∈ ℕ0)
116	114, 115	nn0mulcld 12561	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐽 · 𝐼) ∈ ℕ0)
117	74	ablcmnd 19849	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ CMnd)
118		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (.g‘(𝑅 ↾s 𝑈)) = (.g‘(𝑅 ↾s 𝑈))
119	117, 41, 118	isprimroot 42722	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
120	119	biimpd 232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
121	120	imp 411	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
122	121	simp1d 1158	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)))
123		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ↾s 𝑈) = (𝑅 ↾s 𝑈)
124	123, 47	ressbas2 17288	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ⊆ (Base‘𝑅) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
125	92, 124	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
126	125	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
127	126	eleq2d 2851	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))))
128	122, 127	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑥 ∈ 𝑈)
129	42, 123, 118	submmulg 19175	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ (𝐽 · 𝐼) ∈ ℕ0 ∧ 𝑥 ∈ 𝑈) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥))
130	113, 116, 128, 129	syl3anc 1394	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥))
131	25	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐽 · 𝐼) = (𝐼 · 𝐽))
132	24, 23	mulcld 11217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐼 · 𝐽) ∈ ℂ)
133	3	nncnd 12240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ ℂ)
134	9	zcnd 12692	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑍 ∈ ℂ)
135	133, 134	mulcld 11217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐾 · 𝑍) ∈ ℂ)
136		1cnd 11190	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 1 ∈ ℂ)
137	132, 135, 136	addlsub 11618	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1 ↔ (𝐼 · 𝐽) = (1 − (𝐾 · 𝑍))))
138	13, 137	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 − (𝐾 · 𝑍)))
139	133, 134	mulcomd 11218	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐾 · 𝑍) = (𝑍 · 𝐾))
140	139	oveq2d 7416	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 − (𝐾 · 𝑍)) = (1 − (𝑍 · 𝐾)))
141	138, 140	eqtrd 2800	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 − (𝑍 · 𝐾)))
142	139, 135	eqeltrrd 2866	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑍 · 𝐾) ∈ ℂ)
143	136, 142	negsubd 11563	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 + -(𝑍 · 𝐾)) = (1 − (𝑍 · 𝐾)))
144	143	eqcomd 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 − (𝑍 · 𝐾)) = (1 + -(𝑍 · 𝐾)))
145	141, 144	eqtrd 2800	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 + -(𝑍 · 𝐾)))
146	145	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐼 · 𝐽) = (1 + -(𝑍 · 𝐾)))
147	131, 146	eqtrd 2800	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐽 · 𝐼) = (1 + -(𝑍 · 𝐾)))
148	147	oveq1d 7415	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥) = ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥))
149	76	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ Grp)
150		1zzd 12616	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 1 ∈ ℤ)
151	9	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑍 ∈ ℤ)
152	6	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐾 ∈ ℤ)
153	151, 152	zmulcld 12697	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍 · 𝐾) ∈ ℤ)
154	153	znegcld 12693	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → -(𝑍 · 𝐾) ∈ ℤ)
155	150, 154, 122	3jca 1144	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))))
156		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (Base‘(𝑅 ↾s 𝑈)) = (Base‘(𝑅 ↾s 𝑈))
157		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (+g‘(𝑅 ↾s 𝑈)) = (+g‘(𝑅 ↾s 𝑈))
158	156, 118, 157	mulgdir 19163	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥) = ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)))
159	149, 155, 158	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥) = ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)))
160	156, 118	mulg1 19138	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)) → (1(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
161	122, 160	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (1(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
162		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (invg‘(𝑅 ↾s 𝑈)) = (invg‘(𝑅 ↾s 𝑈))
163	156, 118, 162	mulgneg 19149	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑍 · 𝐾) ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))) → (-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)))
164	149, 153, 122, 163	syl3anc 1394	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)))
165	161, 164	oveq12d 7418	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = (𝑥(+g‘(𝑅 ↾s 𝑈))((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥))))
166	151, 152, 122	3jca 1144	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))))
167	156, 118	mulgass 19168	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑍 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)))
168	149, 166, 167	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)))
169	121	simp2d 1159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)))
170	169	oveq2d 7416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)) = (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
171		eqid 2765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0g‘(𝑅 ↾s 𝑈)) = (0g‘(𝑅 ↾s 𝑈))
172	156, 118, 171	mulgz 19159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ 𝑍 ∈ ℤ) → (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
173	149, 151, 172	syl2anc 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
174	170, 173	eqtrd 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)) = (0g‘(𝑅 ↾s 𝑈)))
175	168, 174	eqtrd 2800	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)))
176	175	fveq2d 6875	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))))
177	171, 162	grpinvid 19056	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ↾s 𝑈) ∈ Grp → ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
178	76, 177	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
179	178	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
180	176, 179	eqtrd 2800	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = (0g‘(𝑅 ↾s 𝑈)))
181	180	oveq2d 7416	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥(+g‘(𝑅 ↾s 𝑈))((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥))) = (𝑥(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
182	149, 77	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ Mnd)
183	156, 157, 171	mndrid 18803	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ↾s 𝑈) ∈ Mnd ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))) → (𝑥(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = 𝑥)
184	182, 122, 183	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = 𝑥)
185	181, 184	eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥(+g‘(𝑅 ↾s 𝑈))((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥))) = 𝑥)
186	165, 185	eqtrd 2800	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = 𝑥)
187	159, 186	eqtrd 2800	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
188	148, 187	eqtrd 2800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
189	130, 188	eqtrd 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = 𝑥)
190	189	ex 417	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = 𝑥))
191	190	imim2d 58	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ (𝑅 PrimRoots 𝐾) → 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥 ∈ (𝑅 PrimRoots 𝐾) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = 𝑥)))
192	73, 191	mpd 16	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = 𝑥))
193	192	imp 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = 𝑥)
194	68, 193	eqtr3d 2802	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)) = 𝑥)
195	65, 194	eqtrd 2800	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)) = 𝑥)
196	51, 195	eqtrd 2800	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = 𝑥)
197	196	ralrimiva 3157	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (𝑅 PrimRoots 𝐾)((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = 𝑥)
198		eqidd 2766	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)) = (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)))
199		simpr 489	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = 𝑦) → 𝑛 = 𝑦)
200	199	oveq2d 7416	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = 𝑦) → (𝐽(.g‘𝑅)𝑛) = (𝐽(.g‘𝑅)𝑦))
201		simpr 489	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ (𝑅 PrimRoots 𝐾))
202	37	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ Mnd)
203	61	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐽 ∈ ℕ0)
204	2, 41, 42	isprimroot 42722	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑦 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑦) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑦) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
205	204	biimpd 232	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) → (𝑦 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑦) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑦) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
206	205	imp 411	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑦 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑦) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑦) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
207	206	simp1d 1158	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ (Base‘𝑅))
208	47, 42	mulgnn0cl 19147	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐽 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐽(.g‘𝑅)𝑦) ∈ (Base‘𝑅))
209	202, 203, 207, 208	syl3anc 1394	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)𝑦) ∈ (Base‘𝑅))
210	198, 200, 201, 209	fvmptd 6987	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦) = (𝐽(.g‘𝑅)𝑦))
211	210	fveq2d 6875	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = (𝐹‘(𝐽(.g‘𝑅)𝑦)))
212	1	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚)))
213		simpr 489	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = (𝐽(.g‘𝑅)𝑦)) → 𝑚 = (𝐽(.g‘𝑅)𝑦))
214	213	oveq2d 7416	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = (𝐽(.g‘𝑅)𝑦)) → (𝐼(.g‘𝑅)𝑚) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
215	2	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
216	3	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℕ)
217	7	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐽 ∈ ℕ)
218	31	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽 gcd 𝐾) = 1)
219	215, 216, 217, 218, 201, 59	primrootscoprmpow 42728	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)𝑦) ∈ (𝑅 PrimRoots 𝐾))
220	39	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐼 ∈ ℕ0)
221	47, 42	mulgnn0cl 19147	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ ℕ0 ∧ (𝐽(.g‘𝑅)𝑦) ∈ (Base‘𝑅)) → (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)) ∈ (Base‘𝑅))
222	202, 220, 209, 221	syl3anc 1394	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)) ∈ (Base‘𝑅))
223	212, 214, 219, 222	fvmptd 6987	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘(𝐽(.g‘𝑅)𝑦)) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
224	220, 203, 207	3jca 1144	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 ∈ ℕ0 ∧ 𝐽 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑅)))
225	47, 42	mulgnn0ass 19167	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ (𝐼 ∈ ℕ0 ∧ 𝐽 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑅))) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
226	202, 224, 225	syl2anc 595	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
227	112	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
228	220, 203	nn0mulcld 12561	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 · 𝐽) ∈ ℕ0)
229	128	ex 417	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → 𝑥 ∈ 𝑈))
230	229	ssrdv 3945	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ 𝑈)
231	71	sseq1d 3970	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) ⊆ 𝑈 ↔ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ 𝑈))
232	230, 231	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ 𝑈)
233	232	sseld 3938	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) → 𝑦 ∈ 𝑈))
234	233	imp 411	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ 𝑈)
235	42, 123, 118	submmulg 19175	. . . . . . . 8 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ (𝐼 · 𝐽) ∈ ℕ0 ∧ 𝑦 ∈ 𝑈) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦))
236	227, 228, 234, 235	syl3anc 1394	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦))
237	145	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 · 𝐽) = (1 + -(𝑍 · 𝐾)))
238	237	oveq1d 7415	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦) = ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦))
239	76	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ Grp)
240		1zzd 12616	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 1 ∈ ℤ)
241	9	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑍 ∈ ℤ)
242	6	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℤ)
243	241, 242	zmulcld 12697	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍 · 𝐾) ∈ ℤ)
244	243	znegcld 12693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → -(𝑍 · 𝐾) ∈ ℤ)
245	232, 125	sseqtrd 3975	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ (Base‘(𝑅 ↾s 𝑈)))
246	245	sseld 3938	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) → 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈))))
247	246	imp 411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)))
248	240, 244, 247	3jca 1144	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈))))
249	156, 118, 157	mulgdir 19163	. . . . . . . . . 10 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦) = ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)))
250	239, 248, 249	syl2anc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦) = ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)))
251	156, 118	mulg1 19138	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)) → (1(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
252	247, 251	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (1(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
253	156, 118, 162	mulgneg 19149	. . . . . . . . . . . . 13 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑍 · 𝐾) ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈))) → (-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)))
254	239, 243, 247, 253	syl3anc 1394	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)))
255	241, 242, 247	3jca 1144	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈))))
256	156, 118	mulgass 19168	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑍 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)))
257	239, 255, 256	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)))
258	117, 41, 118	isprimroot 42722	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
259	258	biimpd 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
260	259	imp 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
261	260	simp2d 1159	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
262	261	ex 417	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈))))
263	71	eleq2d 2851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) ↔ 𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
264	263	imbi1d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑦 ∈ (𝑅 PrimRoots 𝐾) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈))) ↔ (𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))))
265	262, 264	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈))))
266	265	imp 411	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
267	266	oveq2d 7416	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)) = (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
268	239, 241, 172	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
269	267, 268	eqtrd 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)) = (0g‘(𝑅 ↾s 𝑈)))
270	257, 269	eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
271	270	fveq2d 6875	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))))
272	239, 177	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
273	271, 272	eqtrd 2800	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = (0g‘(𝑅 ↾s 𝑈)))
274	254, 273	eqtrd 2800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
275	252, 274	oveq12d 7418	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = (𝑦(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
276	156, 157, 171, 239, 247	grpridd 19027	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑦(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = 𝑦)
277	275, 276	eqtrd 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = 𝑦)
278	250, 277	eqtrd 2800	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
279	238, 278	eqtrd 2800	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
280	236, 279	eqtrd 2800	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = 𝑦)
281	226, 280	eqtr3d 2802	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)) = 𝑦)
282	223, 281	eqtrd 2800	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘(𝐽(.g‘𝑅)𝑦)) = 𝑦)
283	211, 282	eqtrd 2800	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = 𝑦)
284	283	ralrimiva 3157	. 2 ⊢ (𝜑 → ∀𝑦 ∈ (𝑅 PrimRoots 𝐾)(𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = 𝑦)
285	18, 32, 197, 284	2fvidf1od 7286	1 ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)–1-1-onto→(𝑅 PrimRoots 𝐾))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ∀wral 3079  ∃wrex 3089  {crab 3417   ⊆ wss 3907   class class class wbr 5105   ↦ cmpt 5186  –1-1-onto→wf1o 6524  ‘cfv 6525  (class class class)co 7400  ℂcc 11086  1c1 11089   + caddc 11091   · cmul 11093   − cmin 11429  -cneg 11430  ℕcn 12224  ℕ₀cn0 12495  ℤcz 12582   ∥ cdvds 16300   gcd cgcd 16542  Basecbs 17259   ↾_s cress 17280  +_gcplusg 17300  0_gc0g 17482  Mndcmnd 18782  SubMndcsubmnd 18830  Grpcgrp 18990  inv_gcminusg 18991  ._gcmg 19124  CMndccmn 19841  Abelcabl 19842   PrimRoots cprimroots 42720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165  ax-pre-sup 11166

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-sup 9390  df-inf 9391  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-div 11860  df-nn 12225  df-2 12294  df-3 12295  df-n0 12496  df-z 12583  df-uz 12854  df-rp 13008  df-fz 13527  df-fl 13816  df-mod 13894  df-seq 14029  df-exp 14089  df-cj 15140  df-re 15141  df-im 15142  df-sqrt 15276  df-abs 15277  df-dvds 16301  df-gcd 16543  df-sets 17214  df-slot 17232  df-ndx 17244  df-base 17260  df-ress 17281  df-plusg 17313  df-0g 17484  df-mgm 18688  df-sgrp 18767  df-mnd 18783  df-submnd 18832  df-grp 18993  df-minusg 18994  df-mulg 19125  df-cmn 19843  df-abl 19844  df-primroots 42721

This theorem is referenced by:  primrootscoprbij2  42732