Theorem primrootscoprbij 42059

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 12666	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
6	3	nnzd 12666	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℤ)
7		primrootscoprbij.5	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℕ)
8	7	nnzd 12666	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ ℤ)
9		primrootscoprbij.6	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ ℤ)
10	8, 9	jca 511	. . . . . 6 ⊢ (𝜑 → (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ))
11	5, 6, 10	jca31 514	. . . . 5 ⊢ (𝜑 → ((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)))
12		primrootscoprbij.7	. . . . . 6 ⊢ (𝜑 → 1 = ((𝐼 · 𝐽) + (𝐾 · 𝑍)))
13	12	eqcomd 2746	. . . . 5 ⊢ (𝜑 → ((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1)
14	11, 13	jca 511	. . . 4 ⊢ (𝜑 → (((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1))
15		bezoutr1 16616	. . . . 5 ⊢ (((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)) → (((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1 → (𝐼 gcd 𝐾) = 1))
16	15	imp 406	. . . 4 ⊢ ((((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1) → (𝐼 gcd 𝐾) = 1)
17	14, 16	syl 17	. . 3 ⊢ (𝜑 → (𝐼 gcd 𝐾) = 1)
18	1, 2, 3, 4, 17	primrootscoprf 42058	. 2 ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)⟶(𝑅 PrimRoots 𝐾))
19		eqid 2740	. . 3 ⊢ (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)) = (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))
20	8, 6	jca 511	. . . . . 6 ⊢ (𝜑 → (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ))
21	5, 9	jca 511	. . . . . 6 ⊢ (𝜑 → (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ))
22	20, 21	jca 511	. . . . 5 ⊢ (𝜑 → ((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)))
23	7	nncnd 12309	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℂ)
24	4	nncnd 12309	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ ℂ)
25	23, 24	mulcomd 11311	. . . . . . 7 ⊢ (𝜑 → (𝐽 · 𝐼) = (𝐼 · 𝐽))
26	25	oveq1d 7463	. . . . . 6 ⊢ (𝜑 → ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = ((𝐼 · 𝐽) + (𝐾 · 𝑍)))
27	26, 13	eqtrd 2780	. . . . 5 ⊢ (𝜑 → ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1)
28	22, 27	jca 511	. . . 4 ⊢ (𝜑 → (((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1))
29		bezoutr1 16616	. . . . 5 ⊢ (((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)) → (((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1 → (𝐽 gcd 𝐾) = 1))
30	29	imp 406	. . . 4 ⊢ ((((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1) → (𝐽 gcd 𝐾) = 1)
31	28, 30	syl 17	. . 3 ⊢ (𝜑 → (𝐽 gcd 𝐾) = 1)
32	19, 2, 3, 7, 31	primrootscoprf 42058	. 2 ⊢ (𝜑 → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)):(𝑅 PrimRoots 𝐾)⟶(𝑅 PrimRoots 𝐾))
33	1	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚)))
34		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = 𝑥) → 𝑚 = 𝑥)
35	34	oveq2d 7464	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = 𝑥) → (𝐼(.g‘𝑅)𝑚) = (𝐼(.g‘𝑅)𝑥))
36		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑥 ∈ (𝑅 PrimRoots 𝐾))
37	2	cmnmndd 19846	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Mnd)
38	37	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ Mnd)
39	4	nnnn0d 12613	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ ℕ0)
40	39	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐼 ∈ ℕ0)
41	3	nnnn0d 12613	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
42		eqid 2740	. . . . . . . . . . 11 ⊢ (.g‘𝑅) = (.g‘𝑅)
43	2, 41, 42	isprimroot 42050	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
44	43	biimpd 229	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
45	44	imp 406	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
46	45	simp1d 1142	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑥 ∈ (Base‘𝑅))
47		eqid 2740	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
48	47, 42	mulgnn0cl 19130	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ ℕ0 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐼(.g‘𝑅)𝑥) ∈ (Base‘𝑅))
49	38, 40, 46, 48	syl3anc 1371	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)𝑥) ∈ (Base‘𝑅))
50	33, 35, 36, 49	fvmptd 7036	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘𝑥) = (𝐼(.g‘𝑅)𝑥))
51	50	fveq2d 6924	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)))
52		eqidd 2741	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)) = (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)))
53		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = (𝐼(.g‘𝑅)𝑥)) → 𝑛 = (𝐼(.g‘𝑅)𝑥))
54	53	oveq2d 7464	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = (𝐼(.g‘𝑅)𝑥)) → (𝐽(.g‘𝑅)𝑛) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
55	2	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
56	3	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℕ)
57	4	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐼 ∈ ℕ)
58	17	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 gcd 𝐾) = 1)
59		eqid 2740	. . . . . . 7 ⊢ {𝑠 ∈ (Base‘𝑅) ∣ ∃𝑡 ∈ (Base‘𝑅)(𝑡(+g‘𝑅)𝑠) = (0g‘𝑅)} = {𝑠 ∈ (Base‘𝑅) ∣ ∃𝑡 ∈ (Base‘𝑅)(𝑡(+g‘𝑅)𝑠) = (0g‘𝑅)}
60	55, 56, 57, 58, 36, 59	primrootscoprmpow 42056	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)𝑥) ∈ (𝑅 PrimRoots 𝐾))
61	7	nnnn0d 12613	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℕ0)
62	61	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐽 ∈ ℕ0)
63	47, 42	mulgnn0cl 19130	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐽 ∈ ℕ0 ∧ (𝐼(.g‘𝑅)𝑥) ∈ (Base‘𝑅)) → (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)) ∈ (Base‘𝑅))
64	38, 62, 49, 63	syl3anc 1371	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)) ∈ (Base‘𝑅))
65	52, 54, 60, 64	fvmptd 7036	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
66	62, 40, 46	3jca 1128	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝑥 ∈ (Base‘𝑅)))
67	47, 42	mulgnn0ass 19150	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ (𝐽 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝑥 ∈ (Base‘𝑅))) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
68	38, 66, 67	syl2anc 583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
69		primrootscoprbij.8	. . . . . . . . . . . 12 ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}
70	2, 3, 69	primrootsunit 42055	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))
71	70	simpld 494	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
72	71	eleq2d 2830	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) ↔ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
73	72	biimpd 229	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) → 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
74	70	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Abel)
75		ablgrp 19827	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ↾s 𝑈) ∈ Abel → (𝑅 ↾s 𝑈) ∈ Grp)
76	74, 75	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Grp)
77		grpmnd 18980	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ↾s 𝑈) ∈ Grp → (𝑅 ↾s 𝑈) ∈ Mnd)
78	76, 77	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd)
79	37, 78	jca 511	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd))
80	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
81	80	eleq2d 2830	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑓 ∈ 𝑈 ↔ 𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
82	81	biimpd 229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑓 ∈ 𝑈 → 𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
83	82	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑈) → 𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
84		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑓 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑓))
85	84	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑓 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
86	85	rexbidv 3185	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑓 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
87	86	elrab 3708	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑓 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
88	87	biimpi 216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → (𝑓 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
89	88	simpld 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑓 ∈ (Base‘𝑅))
90	83, 89	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑈) → 𝑓 ∈ (Base‘𝑅))
91	90	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑓 ∈ 𝑈 → 𝑓 ∈ (Base‘𝑅)))
92	91	ssrdv 4014	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑅))
93		oveq2 7456	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (0g‘𝑅) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(0g‘𝑅)))
94	93	eqeq1d 2742	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (0g‘𝑅) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
95	94	rexbidv 3185	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (0g‘𝑅) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
96		eqid 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0g‘𝑅) = (0g‘𝑅)
97	47, 96	mndidcl 18787	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ Mnd → (0g‘𝑅) ∈ (Base‘𝑅))
98	37, 97	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅))
99		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → 𝑖 = (0g‘𝑅))
100	99	oveq1d 7463	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → (𝑖(+g‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)))
101	100	eqeq1d 2742	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → ((𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅) ↔ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
102		eqid 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (+g‘𝑅) = (+g‘𝑅)
103	47, 102, 96	mndlid 18792	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
104	37, 98, 103	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
105	98, 101, 104	rspcedvd 3637	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
106	95, 98, 105	elrabd 3710	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
107	80	eleq2d 2830	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0g‘𝑅) ∈ 𝑈 ↔ (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
108	106, 107	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0g‘𝑅) ∈ 𝑈)
109	92, 108	jca 511	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈))
110	79, 109	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
111	47, 96	issubmndb 18840	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ (SubMnd‘𝑅) ↔ ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
112	110, 111	sylibr 234	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ (SubMnd‘𝑅))
113	112	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
114	61	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐽 ∈ ℕ0)
115	39	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐼 ∈ ℕ0)
116	114, 115	nn0mulcld 12618	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐽 · 𝐼) ∈ ℕ0)
117	74	ablcmnd 19830	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ CMnd)
118		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (.g‘(𝑅 ↾s 𝑈)) = (.g‘(𝑅 ↾s 𝑈))
119	117, 41, 118	isprimroot 42050	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
120	119	biimpd 229	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
121	120	imp 406	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
122	121	simp1d 1142	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)))
123		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ↾s 𝑈) = (𝑅 ↾s 𝑈)
124	123, 47	ressbas2 17296	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ⊆ (Base‘𝑅) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
125	92, 124	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
126	125	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
127	126	eleq2d 2830	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))))
128	122, 127	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑥 ∈ 𝑈)
129	42, 123, 118	submmulg 19158	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ (𝐽 · 𝐼) ∈ ℕ0 ∧ 𝑥 ∈ 𝑈) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥))
130	113, 116, 128, 129	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥))
131	25	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐽 · 𝐼) = (𝐼 · 𝐽))
132	24, 23	mulcld 11310	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐼 · 𝐽) ∈ ℂ)
133	3	nncnd 12309	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ ℂ)
134	9	zcnd 12748	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑍 ∈ ℂ)
135	133, 134	mulcld 11310	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐾 · 𝑍) ∈ ℂ)
136		1cnd 11285	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 1 ∈ ℂ)
137	132, 135, 136	addlsub 11706	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1 ↔ (𝐼 · 𝐽) = (1 − (𝐾 · 𝑍))))
138	13, 137	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 − (𝐾 · 𝑍)))
139	133, 134	mulcomd 11311	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐾 · 𝑍) = (𝑍 · 𝐾))
140	139	oveq2d 7464	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 − (𝐾 · 𝑍)) = (1 − (𝑍 · 𝐾)))
141	138, 140	eqtrd 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 − (𝑍 · 𝐾)))
142	139, 135	eqeltrrd 2845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑍 · 𝐾) ∈ ℂ)
143	136, 142	negsubd 11653	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 + -(𝑍 · 𝐾)) = (1 − (𝑍 · 𝐾)))
144	143	eqcomd 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 − (𝑍 · 𝐾)) = (1 + -(𝑍 · 𝐾)))
145	141, 144	eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 + -(𝑍 · 𝐾)))
146	145	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐼 · 𝐽) = (1 + -(𝑍 · 𝐾)))
147	131, 146	eqtrd 2780	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐽 · 𝐼) = (1 + -(𝑍 · 𝐾)))
148	147	oveq1d 7463	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥) = ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥))
149	76	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ Grp)
150		1zzd 12674	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 1 ∈ ℤ)
151	9	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑍 ∈ ℤ)
152	6	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐾 ∈ ℤ)
153	151, 152	zmulcld 12753	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍 · 𝐾) ∈ ℤ)
154	153	znegcld 12749	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → -(𝑍 · 𝐾) ∈ ℤ)
155	150, 154, 122	3jca 1128	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))))
156		eqid 2740	. . . . . . . . . . . . . . 15 ⊢ (Base‘(𝑅 ↾s 𝑈)) = (Base‘(𝑅 ↾s 𝑈))
157		eqid 2740	. . . . . . . . . . . . . . 15 ⊢ (+g‘(𝑅 ↾s 𝑈)) = (+g‘(𝑅 ↾s 𝑈))
158	156, 118, 157	mulgdir 19146	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥) = ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)))
159	149, 155, 158	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥) = ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)))
160	156, 118	mulg1 19121	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)) → (1(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
161	122, 160	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (1(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
162		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (invg‘(𝑅 ↾s 𝑈)) = (invg‘(𝑅 ↾s 𝑈))
163	156, 118, 162	mulgneg 19132	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑍 · 𝐾) ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))) → (-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)))
164	149, 153, 122, 163	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)))
165	161, 164	oveq12d 7466	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = (𝑥(+g‘(𝑅 ↾s 𝑈))((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥))))
166	151, 152, 122	3jca 1128	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))))
167	156, 118	mulgass 19151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑍 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)))
168	149, 166, 167	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)))
169	121	simp2d 1143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)))
170	169	oveq2d 7464	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)) = (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
171		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0g‘(𝑅 ↾s 𝑈)) = (0g‘(𝑅 ↾s 𝑈))
172	156, 118, 171	mulgz 19142	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ 𝑍 ∈ ℤ) → (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
173	149, 151, 172	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
174	170, 173	eqtrd 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)) = (0g‘(𝑅 ↾s 𝑈)))
175	168, 174	eqtrd 2780	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)))
176	175	fveq2d 6924	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))))
177	171, 162	grpinvid 19039	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ↾s 𝑈) ∈ Grp → ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
178	76, 177	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
179	178	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
180	176, 179	eqtrd 2780	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = (0g‘(𝑅 ↾s 𝑈)))
181	180	oveq2d 7464	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥(+g‘(𝑅 ↾s 𝑈))((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥))) = (𝑥(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
182	149, 77	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ Mnd)
183	156, 157, 171	mndrid 18793	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ↾s 𝑈) ∈ Mnd ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))) → (𝑥(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = 𝑥)
184	182, 122, 183	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = 𝑥)
185	181, 184	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥(+g‘(𝑅 ↾s 𝑈))((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥))) = 𝑥)
186	165, 185	eqtrd 2780	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = 𝑥)
187	159, 186	eqtrd 2780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
188	148, 187	eqtrd 2780	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
189	130, 188	eqtrd 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = 𝑥)
190	189	ex 412	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = 𝑥))
191	190	imim2d 57	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ (𝑅 PrimRoots 𝐾) → 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥 ∈ (𝑅 PrimRoots 𝐾) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = 𝑥)))
192	73, 191	mpd 15	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = 𝑥))
193	192	imp 406	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘𝑅)𝑥) = 𝑥)
194	68, 193	eqtr3d 2782	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)) = 𝑥)
195	65, 194	eqtrd 2780	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)) = 𝑥)
196	51, 195	eqtrd 2780	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = 𝑥)
197	196	ralrimiva 3152	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (𝑅 PrimRoots 𝐾)((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = 𝑥)
198		eqidd 2741	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)) = (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)))
199		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = 𝑦) → 𝑛 = 𝑦)
200	199	oveq2d 7464	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = 𝑦) → (𝐽(.g‘𝑅)𝑛) = (𝐽(.g‘𝑅)𝑦))
201		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ (𝑅 PrimRoots 𝐾))
202	37	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ Mnd)
203	61	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐽 ∈ ℕ0)
204	2, 41, 42	isprimroot 42050	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑦 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑦) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑦) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
205	204	biimpd 229	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) → (𝑦 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑦) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑦) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
206	205	imp 406	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑦 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑦) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑦) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
207	206	simp1d 1142	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ (Base‘𝑅))
208	47, 42	mulgnn0cl 19130	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐽 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐽(.g‘𝑅)𝑦) ∈ (Base‘𝑅))
209	202, 203, 207, 208	syl3anc 1371	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)𝑦) ∈ (Base‘𝑅))
210	198, 200, 201, 209	fvmptd 7036	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦) = (𝐽(.g‘𝑅)𝑦))
211	210	fveq2d 6924	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = (𝐹‘(𝐽(.g‘𝑅)𝑦)))
212	1	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚)))
213		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = (𝐽(.g‘𝑅)𝑦)) → 𝑚 = (𝐽(.g‘𝑅)𝑦))
214	213	oveq2d 7464	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = (𝐽(.g‘𝑅)𝑦)) → (𝐼(.g‘𝑅)𝑚) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
215	2	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
216	3	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℕ)
217	7	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐽 ∈ ℕ)
218	31	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽 gcd 𝐾) = 1)
219	215, 216, 217, 218, 201, 59	primrootscoprmpow 42056	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)𝑦) ∈ (𝑅 PrimRoots 𝐾))
220	39	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐼 ∈ ℕ0)
221	47, 42	mulgnn0cl 19130	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ ℕ0 ∧ (𝐽(.g‘𝑅)𝑦) ∈ (Base‘𝑅)) → (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)) ∈ (Base‘𝑅))
222	202, 220, 209, 221	syl3anc 1371	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)) ∈ (Base‘𝑅))
223	212, 214, 219, 222	fvmptd 7036	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘(𝐽(.g‘𝑅)𝑦)) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
224	220, 203, 207	3jca 1128	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 ∈ ℕ0 ∧ 𝐽 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑅)))
225	47, 42	mulgnn0ass 19150	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ (𝐼 ∈ ℕ0 ∧ 𝐽 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑅))) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
226	202, 224, 225	syl2anc 583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
227	112	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
228	220, 203	nn0mulcld 12618	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 · 𝐽) ∈ ℕ0)
229	128	ex 412	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → 𝑥 ∈ 𝑈))
230	229	ssrdv 4014	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ 𝑈)
231	71	sseq1d 4040	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) ⊆ 𝑈 ↔ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ 𝑈))
232	230, 231	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ 𝑈)
233	232	sseld 4007	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) → 𝑦 ∈ 𝑈))
234	233	imp 406	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ 𝑈)
235	42, 123, 118	submmulg 19158	. . . . . . . 8 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ (𝐼 · 𝐽) ∈ ℕ0 ∧ 𝑦 ∈ 𝑈) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦))
236	227, 228, 234, 235	syl3anc 1371	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦))
237	145	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 · 𝐽) = (1 + -(𝑍 · 𝐾)))
238	237	oveq1d 7463	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦) = ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦))
239	76	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ Grp)
240		1zzd 12674	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 1 ∈ ℤ)
241	9	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑍 ∈ ℤ)
242	6	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℤ)
243	241, 242	zmulcld 12753	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍 · 𝐾) ∈ ℤ)
244	243	znegcld 12749	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → -(𝑍 · 𝐾) ∈ ℤ)
245	232, 125	sseqtrd 4049	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ (Base‘(𝑅 ↾s 𝑈)))
246	245	sseld 4007	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) → 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈))))
247	246	imp 406	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)))
248	240, 244, 247	3jca 1128	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈))))
249	156, 118, 157	mulgdir 19146	. . . . . . . . . 10 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦) = ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)))
250	239, 248, 249	syl2anc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦) = ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)))
251	156, 118	mulg1 19121	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)) → (1(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
252	247, 251	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (1(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
253	156, 118, 162	mulgneg 19132	. . . . . . . . . . . . 13 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑍 · 𝐾) ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈))) → (-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)))
254	239, 243, 247, 253	syl3anc 1371	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)))
255	241, 242, 247	3jca 1128	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈))))
256	156, 118	mulgass 19151	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑍 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)))
257	239, 255, 256	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)))
258	117, 41, 118	isprimroot 42050	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
259	258	biimpd 229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
260	259	imp 406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
261	260	simp2d 1143	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
262	261	ex 412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈))))
263	71	eleq2d 2830	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) ↔ 𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
264	263	imbi1d 341	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑦 ∈ (𝑅 PrimRoots 𝐾) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈))) ↔ (𝑦 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))))
265	262, 264	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈))))
266	265	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
267	266	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)) = (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
268	239, 241, 172	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
269	267, 268	eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)) = (0g‘(𝑅 ↾s 𝑈)))
270	257, 269	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
271	270	fveq2d 6924	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))))
272	239, 177	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈)))
273	271, 272	eqtrd 2780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = (0g‘(𝑅 ↾s 𝑈)))
274	254, 273	eqtrd 2780	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
275	252, 274	oveq12d 7466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = (𝑦(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
276	156, 157, 171, 239, 247	grpridd 19010	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑦(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = 𝑦)
277	275, 276	eqtrd 2780	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = 𝑦)
278	250, 277	eqtrd 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
279	238, 278	eqtrd 2780	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
280	236, 279	eqtrd 2780	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = 𝑦)
281	226, 280	eqtr3d 2782	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)) = 𝑦)
282	223, 281	eqtrd 2780	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘(𝐽(.g‘𝑅)𝑦)) = 𝑦)
283	211, 282	eqtrd 2780	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = 𝑦)
284	283	ralrimiva 3152	. 2 ⊢ (𝜑 → ∀𝑦 ∈ (𝑅 PrimRoots 𝐾)(𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = 𝑦)
285	18, 32, 197, 284	2fvidf1od 7334	1 ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)–1-1-onto→(𝑅 PrimRoots 𝐾))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ∃wrex 3076  {crab 3443   ⊆ wss 3976   class class class wbr 5166   ↦ cmpt 5249  –1-1-onto→wf1o 6572  ‘cfv 6573  (class class class)co 7448  ℂcc 11182  1c1 11185   + caddc 11187   · cmul 11189   − cmin 11520  -cneg 11521  ℕcn 12293  ℕ₀cn0 12553  ℤcz 12639   ∥ cdvds 16302   gcd cgcd 16540  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  ax-pre-sup 11262

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-sup 9511  df-inf 9512  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-n0 12554  df-z 12640  df-uz 12904  df-rp 13058  df-fz 13568  df-fl 13843  df-mod 13921  df-seq 14053  df-exp 14113  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-dvds 16303  df-gcd 16541  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:  primrootscoprbij2  42060