Theorem primrootscoprbij 43245

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 12722	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
6	3	nnzd 12722	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℤ)
7		primrootscoprbij.5	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℕ)
8	7	nnzd 12722	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ ℤ)
9		primrootscoprbij.6	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ ℤ)
10	8, 9	jca 521	. . . . . 6 ⊢ (𝜑 → (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ))
11	5, 6, 10	jca31 524	. . . . 5 ⊢ (𝜑 → ((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)))
12		primrootscoprbij.7	. . . . . 6 ⊢ (𝜑 → 1 = ((𝐼 · 𝐽) + (𝐾 · 𝑍)))
13	12	eqcomd 2766	. . . . 5 ⊢ (𝜑 → ((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1)
14	11, 13	jca 521	. . . 4 ⊢ (𝜑 → (((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1))
15		bezoutr1 16749	. . . . 5 ⊢ (((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)) → (((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1 → (𝐼 gcd 𝐾) = 1))
16	15	imp 412	. . . 4 ⊢ ((((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1) → (𝐼 gcd 𝐾) = 1)
17	14, 16	syl 18	. . 3 ⊢ (𝜑 → (𝐼 gcd 𝐾) = 1)
18	1, 2, 3, 4, 17	primrootscoprf 43244	. 2 ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)⟶(𝑅 PrimRoots 𝐾))
19		eqid 2760	. . 3 ⊢ (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)) = (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))
20	8, 6	jca 521	. . . . . 6 ⊢ (𝜑 → (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ))
21	5, 9	jca 521	. . . . . 6 ⊢ (𝜑 → (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ))
22	20, 21	jca 521	. . . . 5 ⊢ (𝜑 → ((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)))
23	7	nncnd 12354	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℂ)
24	4	nncnd 12354	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ ℂ)
25	23, 24	mulcomd 11333	. . . . . . 7 ⊢ (𝜑 → (𝐽 · 𝐼) = (𝐼 · 𝐽))
26	25	oveq1d 7435	. . . . . 6 ⊢ (𝜑 → ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = ((𝐼 · 𝐽) + (𝐾 · 𝑍)))
27	26, 13	eqtrd 2795	. . . . 5 ⊢ (𝜑 → ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1)
28	22, 27	jca 521	. . . 4 ⊢ (𝜑 → (((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1))
29		bezoutr1 16749	. . . . 5 ⊢ (((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)) → (((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1 → (𝐽 gcd 𝐾) = 1))
30	29	imp 412	. . . 4 ⊢ ((((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1) → (𝐽 gcd 𝐾) = 1)
31	28, 30	syl 18	. . 3 ⊢ (𝜑 → (𝐽 gcd 𝐾) = 1)
32	19, 2, 3, 7, 31	primrootscoprf 43244	. 2 ⊢ (𝜑 → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)):(𝑅 PrimRoots 𝐾)⟶(𝑅 PrimRoots 𝐾))
33	1	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚)))
34		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = 𝑥) → 𝑚 = 𝑥)
35	34	oveq2d 7436	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = 𝑥) → (𝐼(.g‘𝑅)𝑚) = (𝐼(.g‘𝑅)𝑥))
36		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑥 ∈ (𝑅 PrimRoots 𝐾))
37	2	cmnmndd 20023	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Mnd)
38	37	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ Mnd)
39	4	nnnn0d 12670	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ ℕ0)
40	39	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐼 ∈ ℕ0)
41	3	nnnn0d 12670	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
42		eqid 2760	. . . . . . . . . . 11 ⊢ (.g‘𝑅) = (.g‘𝑅)
43	2, 41, 42	isprimroot 43236	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
44	43	biimpd 232	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
45	44	imp 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
46	45	simp1d 1160	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑥 ∈ (Base‘𝑅))
47		eqid 2760	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
48	47, 42	mulgnn0cl 19305	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ ℕ0 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐼(.g‘𝑅)𝑥) ∈ (Base‘𝑅))
49	38, 40, 46, 48	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)𝑥) ∈ (Base‘𝑅))
50	33, 35, 36, 49	fvmptd 7001	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘𝑥) = (𝐼(.g‘𝑅)𝑥))
51	50	fveq2d 6889	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)))
52		eqidd 2761	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)) = (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)))
53		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = (𝐼(.g‘𝑅)𝑥)) → 𝑛 = (𝐼(.g‘𝑅)𝑥))
54	53	oveq2d 7436	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = (𝐼(.g‘𝑅)𝑥)) → (𝐽(.g‘𝑅)𝑛) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
55	2	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
56	3	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℕ)
57	4	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐼 ∈ ℕ)
58	17	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 gcd 𝐾) = 1)
59		eqid 2760	. . . . . . 7 ⊢ {𝑠 ∈ (Base‘𝑅) ∣ ∃𝑡 ∈ (Base‘𝑅)(𝑡(+g‘𝑅)𝑠) = (0g‘𝑅)} = {𝑠 ∈ (Base‘𝑅) ∣ ∃𝑡 ∈ (Base‘𝑅)(𝑡(+g‘𝑅)𝑠) = (0g‘𝑅)}
60	55, 56, 57, 58, 36, 59	primrootscoprmpow 43242	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)𝑥) ∈ (𝑅 PrimRoots 𝐾))
61	7	nnnn0d 12670	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℕ0)
62	61	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐽 ∈ ℕ0)
63	47, 42	mulgnn0cl 19305	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐽 ∈ ℕ0 ∧ (𝐼(.g‘𝑅)𝑥) ∈ (Base‘𝑅)) → (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)) ∈ (Base‘𝑅))
64	38, 62, 49, 63	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)) ∈ (Base‘𝑅))
65	52, 54, 60, 64	fvmptd 7001	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
66	62, 40, 46	3jca 1146	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝑥 ∈ (Base‘𝑅)))
67	47, 42	mulgnn0ass 19325	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ (𝐽 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝑥 ∈ (Base‘𝑅))) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
68	38, 66, 67	syl2anc 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
69		primrootscoprbij.8	. . . . . . . . . . . 12 ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}
70	2, 3, 69	primrootsunit 43241	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))
71	70	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
72	71	eleq2d 2846	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) ↔ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
73	72	biimpd 232	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) → 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
74	70	simprd 501	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Abel)
75		ablgrp 20004	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ↾s 𝑈) ∈ Abel → (𝑅 ↾s 𝑈) ∈ Grp)
76	74, 75	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Grp)
77		grpmnd 19156	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ↾s 𝑈) ∈ Grp → (𝑅 ↾s 𝑈) ∈ Mnd)
78	76, 77	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd)
79	37, 78	jca 521	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd))
80	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
81	80	eleq2d 2846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑓 ∈ 𝑈 ↔ 𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
82	81	biimpd 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑓 ∈ 𝑈 → 𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
83	82	imp 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑈) → 𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
84		oveq2 7428	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑓 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑓))
85	84	eqeq1d 2762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑓 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
86	85	rexbidv 3186	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑓 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
87	86	elrab 3644	. . . . . . . . . . . . . . . . . . . . 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 500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑓 ∈ (Base‘𝑅))
90	83, 89	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑈) → 𝑓 ∈ (Base‘𝑅))
91	90	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑓 ∈ 𝑈 → 𝑓 ∈ (Base‘𝑅)))
92	91	ssrdv 3914	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑅))
93		oveq2 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (0g‘𝑅) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(0g‘𝑅)))
94	93	eqeq1d 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (0g‘𝑅) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
95	94	rexbidv 3186	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (0g‘𝑅) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
96		eqid 2760	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0g‘𝑅) = (0g‘𝑅)
97	47, 96	mndidcl 18944	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ Mnd → (0g‘𝑅) ∈ (Base‘𝑅))
98	37, 97	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅))
99		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → 𝑖 = (0g‘𝑅))
100	99	oveq1d 7435	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → (𝑖(+g‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)))
101	100	eqeq1d 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → ((𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅) ↔ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
102		eqid 2760	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (+g‘𝑅) = (+g‘𝑅)
103	47, 102, 96	mndlid 18949	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
104	37, 98, 103	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
105	98, 101, 104	rspcedvd 3578	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
106	95, 98, 105	elrabd 3646	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
107	80	eleq2d 2846	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0g‘𝑅) ∈ 𝑈 ↔ (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
108	106, 107	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0g‘𝑅) ∈ 𝑈)
109	92, 108	jca 521	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈))
110	79, 109	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
111	47, 96	issubmndb 19005	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ (SubMnd‘𝑅) ↔ ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
112	110, 111	sylibr 237	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ (SubMnd‘𝑅))
113	112	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
114	61	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐽 ∈ ℕ0)
115	39	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐼 ∈ ℕ0)
116	114, 115	nn0mulcld 12675	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐽 · 𝐼) ∈ ℕ0)
117	74	ablcmnd 20007	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ CMnd)
118		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (.g‘(𝑅 ↾s 𝑈)) = (.g‘(𝑅 ↾s 𝑈))
119	117, 41, 118	isprimroot 43236	. . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
122	121	simp1d 1160	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)))
123		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ↾s 𝑈) = (𝑅 ↾s 𝑈)
124	123, 47	ressbas2 17421	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ⊆ (Base‘𝑅) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
125	92, 124	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
126	125	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
127	126	eleq2d 2846	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))))
128	122, 127	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑥 ∈ 𝑈)
129	42, 123, 118	submmulg 19333	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ (𝐽 · 𝐼) ∈ ℕ0 ∧ 𝑥 ∈ 𝑈) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥))
130	113, 116, 128, 129	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥))
131	25	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐽 · 𝐼) = (𝐼 · 𝐽))
132	24, 23	mulcld 11332	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐼 · 𝐽) ∈ ℂ)
133	3	nncnd 12354	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ ℂ)
134	9	zcnd 12807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑍 ∈ ℂ)
135	133, 134	mulcld 11332	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐾 · 𝑍) ∈ ℂ)
136		1cnd 11305	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 1 ∈ ℂ)
137	132, 135, 136	addlsub 11735	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1 ↔ (𝐼 · 𝐽) = (1 − (𝐾 · 𝑍))))
138	13, 137	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 − (𝐾 · 𝑍)))
139	133, 134	mulcomd 11333	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐾 · 𝑍) = (𝑍 · 𝐾))
140	139	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 − (𝐾 · 𝑍)) = (1 − (𝑍 · 𝐾)))
141	138, 140	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 − (𝑍 · 𝐾)))
142	139, 135	eqeltrrd 2861	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑍 · 𝐾) ∈ ℂ)
143	136, 142	negsubd 11678	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 + -(𝑍 · 𝐾)) = (1 − (𝑍 · 𝐾)))
144	143	eqcomd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 − (𝑍 · 𝐾)) = (1 + -(𝑍 · 𝐾)))
145	141, 144	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 + -(𝑍 · 𝐾)))
146	145	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐼 · 𝐽) = (1 + -(𝑍 · 𝐾)))
147	131, 146	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐽 · 𝐼) = (1 + -(𝑍 · 𝐾)))
148	147	oveq1d 7435	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥) = ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥))
149	76	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ Grp)
150		1zzd 12730	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 1 ∈ ℤ)
151	9	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑍 ∈ ℤ)
152	6	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐾 ∈ ℤ)
153	151, 152	zmulcld 12812	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍 · 𝐾) ∈ ℤ)
154	153	znegcld 12808	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → -(𝑍 · 𝐾) ∈ ℤ)
155	150, 154, 122	3jca 1146	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))))
156		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (Base‘(𝑅 ↾s 𝑈)) = (Base‘(𝑅 ↾s 𝑈))
157		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (+g‘(𝑅 ↾s 𝑈)) = (+g‘(𝑅 ↾s 𝑈))
158	156, 118, 157	mulgdir 19321	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥) = ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))( -(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)))
159	149, 155, 158	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥) = ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))( -(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)))
160	156, 118	mulg1 19296	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)) → (1(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
161	122, 160	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (1(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
162		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (invg‘(𝑅 ↾s 𝑈)) = (invg‘(𝑅 ↾s 𝑈))
163	156, 118, 162	mulgneg 19307	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑍 · 𝐾) ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))) → ( -(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)))
164	149, 153, 122, 163	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ( -(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)))
165	161, 164	oveq12d 7438	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))( -(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = (𝑥(+g‘(𝑅 ↾s 𝑈))((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥))))
166	151, 152, 122	3jca 1146	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))))
167	156, 118	mulgass 19326	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑍 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)))
168	149, 166, 167	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)))
169	121	simp2d 1161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)))
170	169	oveq2d 7436	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)) = (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
171		eqid 2760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0g‘(𝑅 ↾s 𝑈)) = (0g‘(𝑅 ↾s 𝑈))
172	156, 118, 171	mulgz 19317	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ 𝑍 ∈ ℤ) → (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
173	149, 151, 172	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
174	170, 173	eqtrd 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)) = (0g‘(𝑅 ↾s 𝑈)))
175	168, 174	eqtrd 2795	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)))
176	175	fveq2d 6889	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))))
177	171, 162	grpinvid 19215	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ↾s 𝑈) ∈ Grp → ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
178	76, 177	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
179	178	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
180	176, 179	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = (0g‘(𝑅 ↾s 𝑈)))
181	180	oveq2d 7436	. . . . . . . . . . . . . . 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 18950	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ↾s 𝑈) ∈ Mnd ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))) → (𝑥(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = 𝑥)
184	182, 122, 183	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = 𝑥)
185	181, 184	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥(+g‘(𝑅 ↾s 𝑈))((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥))) = 𝑥)
186	165, 185	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))( -(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = 𝑥)
187	159, 186	eqtrd 2795	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
188	148, 187	eqtrd 2795	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
189	130, 188	eqtrd 2795	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = 𝑥)
190	189	ex 418	. . . . . . . . 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 412	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = 𝑥)
194	68, 193	eqtr3d 2797	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)) = 𝑥)
195	65, 194	eqtrd 2795	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)) = 𝑥)
196	51, 195	eqtrd 2795	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = 𝑥)
197	196	ralrimiva 3154	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (𝑅 PrimRoots 𝐾)((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = 𝑥)
198		eqidd 2761	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)) = (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)))
199		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = 𝑦) → 𝑛 = 𝑦)
200	199	oveq2d 7436	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = 𝑦) → (𝐽(.g‘𝑅)𝑛) = (𝐽(.g‘𝑅)𝑦))
201		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ (𝑅 PrimRoots 𝐾))
202	37	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ Mnd)
203	61	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐽 ∈ ℕ0)
204	2, 41, 42	isprimroot 43236	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑦 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑦) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑦) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
205	204	biimpd 232	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) → (𝑦 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑦) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑦) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
206	205	imp 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑦 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑦) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑦) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
207	206	simp1d 1160	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ (Base‘𝑅))
208	47, 42	mulgnn0cl 19305	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐽 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐽(.g‘𝑅)𝑦) ∈ (Base‘𝑅))
209	202, 203, 207, 208	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)𝑦) ∈ (Base‘𝑅))
210	198, 200, 201, 209	fvmptd 7001	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦) = (𝐽(.g‘𝑅)𝑦))
211	210	fveq2d 6889	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = (𝐹‘(𝐽(.g‘𝑅)𝑦)))
212	1	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚)))
213		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = (𝐽(.g‘𝑅)𝑦)) → 𝑚 = (𝐽(.g‘𝑅)𝑦))
214	213	oveq2d 7436	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = (𝐽(.g‘𝑅)𝑦)) → (𝐼(.g‘𝑅)𝑚) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
215	2	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
216	3	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℕ)
217	7	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐽 ∈ ℕ)
218	31	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽 gcd 𝐾) = 1)
219	215, 216, 217, 218, 201, 59	primrootscoprmpow 43242	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)𝑦) ∈ (𝑅 PrimRoots 𝐾))
220	39	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐼 ∈ ℕ0)
221	47, 42	mulgnn0cl 19305	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ ℕ0 ∧ (𝐽(.g‘𝑅)𝑦) ∈ (Base‘𝑅)) → (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)) ∈ (Base‘𝑅))
222	202, 220, 209, 221	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)) ∈ (Base‘𝑅))
223	212, 214, 219, 222	fvmptd 7001	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘(𝐽(.g‘𝑅)𝑦)) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
224	220, 203, 207	3jca 1146	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 ∈ ℕ0 ∧ 𝐽 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑅)))
225	47, 42	mulgnn0ass 19325	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ (𝐼 ∈ ℕ0 ∧ 𝐽 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑅))) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
226	202, 224, 225	syl2anc 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
227	112	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
228	220, 203	nn0mulcld 12675	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 · 𝐽) ∈ ℕ0)
229	128	ex 418	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → 𝑥 ∈ 𝑈))
230	229	ssrdv 3914	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ 𝑈)
231	71	sseq1d 3939	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) ⊆ 𝑈 ↔ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ 𝑈))
232	230, 231	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ 𝑈)
233	232	sseld 3907	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) → 𝑦 ∈ 𝑈))
234	233	imp 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ 𝑈)
235	42, 123, 118	submmulg 19333	. . . . . . . 8 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ (𝐼 · 𝐽) ∈ ℕ0 ∧ 𝑦 ∈ 𝑈) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦))
236	227, 228, 234, 235	syl3anc 1398	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦))
237	145	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 · 𝐽) = (1 + -(𝑍 · 𝐾)))
238	237	oveq1d 7435	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦) = ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦))
239	76	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ Grp)
240		1zzd 12730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 1 ∈ ℤ)
241	9	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑍 ∈ ℤ)
242	6	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℤ)
243	241, 242	zmulcld 12812	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍 · 𝐾) ∈ ℤ)
244	243	znegcld 12808	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → -(𝑍 · 𝐾) ∈ ℤ)
245	232, 125	sseqtrd 3944	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ (Base‘(𝑅 ↾s 𝑈)))
246	245	sseld 3907	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) → 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈))))
247	246	imp 412	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)))
248	240, 244, 247	3jca 1146	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈))))
249	156, 118, 157	mulgdir 19321	. . . . . . . . . 10 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦) = ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))( -(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)))
250	239, 248, 249	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦) = ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))( -(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)))
251	156, 118	mulg1 19296	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)) → (1(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
252	247, 251	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (1(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
253	156, 118, 162	mulgneg 19307	. . . . . . . . . . . . 13 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑍 · 𝐾) ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈))) → ( -(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)))
254	239, 243, 247, 253	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ( -(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)))
255	241, 242, 247	3jca 1146	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈))))
256	156, 118	mulgass 19326	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑍 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)))
257	239, 255, 256	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)))
258	117, 41, 118	isprimroot 43236	. . . . . . . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
261	260	simp2d 1161	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
262	261	ex 418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈))))
263	71	eleq2d 2846	. . . . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
267	266	oveq2d 7436	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)) = (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
268	239, 241, 172	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
269	267, 268	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)) = (0g‘(𝑅 ↾s 𝑈)))
270	257, 269	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
271	270	fveq2d 6889	. . . . . . . . . . . . 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 2795	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = (0g‘(𝑅 ↾s 𝑈)))
274	254, 273	eqtrd 2795	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ( -(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
275	252, 274	oveq12d 7438	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))( -(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = (𝑦(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
276	156, 157, 171, 239, 247	grpridd 19186	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑦(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = 𝑦)
277	275, 276	eqtrd 2795	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))( -(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = 𝑦)
278	250, 277	eqtrd 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
279	238, 278	eqtrd 2795	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
280	236, 279	eqtrd 2795	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = 𝑦)
281	226, 280	eqtr3d 2797	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)) = 𝑦)
282	223, 281	eqtrd 2795	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘(𝐽(.g‘𝑅)𝑦)) = 𝑦)
283	211, 282	eqtrd 2795	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = 𝑦)
284	283	ralrimiva 3154	. 2 ⊢ (𝜑 → ∀𝑦 ∈ (𝑅 PrimRoots 𝐾)(𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = 𝑦)
285	18, 32, 197, 284	2fvidf1od 7306	1 ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)–1-1-onto→(𝑅 PrimRoots 𝐾))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086  {crab 3412   ⊆ wss 3895   class class class wbr 5102   ↦ cmpt 5185  –1-1-onto→wf1o 6537  ‘cfv 6538  (class class class)co 7420  ℂcc 11201  1c1 11204   + caddc 11206   · cmul 11208   − cmin 11544   -cneg 11545  ℕcn 12338  ℕ₀cn0 12609  ℤcz 12696   ∥ cdvds 16427   gcd cgcd 16669  Basecbs 17392   ↾_s cress 17413  +_gcplusg 17433  0_gc0g 17615  Mndcmnd 18928  SubMndcsubmnd 18982  Grpcgrp 19149  inv_gcminusg 19150  ._gcmg 19282  CMndccmn 19999  Abelcabl 20000   PrimRoots cprimroots 43234

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11259  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279  ax-pre-mulgt0 11280  ax-pre-sup 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-er 8720  df-en 8977  df-dom 8978  df-sdom 8979  df-sup 9437  df-inf 9438  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-sub 11546  df-neg 11547  df-div 11977  df-nn 12339  df-2 12408  df-3 12409  df-n0 12610  df-z 12697  df-uz 12969  df-rp 13124  df-fz 13643  df-fl 13935  df-mod 14013  df-seq 14148  df-exp 14208  df-cj 15271  df-re 15272  df-im 15273  df-sqrt 15407  df-abs 15408  df-dvds 16428  df-gcd 16670  df-sets 17347  df-slot 17365  df-ndx 17377  df-base 17393  df-ress 17414  df-plusg 17446  df-0g 17617  df-mgm 18821  df-sgrp 18913  df-mnd 18929  df-submnd 18984  df-grp 19152  df-minusg 19153  df-mulg 19283  df-cmn 20001  df-abl 20002  df-primroots 43235

This theorem is used by:  primrootscoprbij2  43246