Theorem primrootscoprbij 43120

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 12700	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
6	3	nnzd 12700	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℤ)
7		primrootscoprbij.5	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℕ)
8	7	nnzd 12700	. . . . . . 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 2767	. . . . 5 ⊢ (𝜑 → ((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1)
14	11, 13	jca 521	. . . 4 ⊢ (𝜑 → (((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1))
15		bezoutr1 16724	. . . . 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 43119	. 2 ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)⟶(𝑅 PrimRoots 𝐾))
19		eqid 2761	. . 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 12332	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℂ)
24	4	nncnd 12332	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ ℂ)
25	23, 24	mulcomd 11311	. . . . . . 7 ⊢ (𝜑 → (𝐽 · 𝐼) = (𝐼 · 𝐽))
26	25	oveq1d 7427	. . . . . 6 ⊢ (𝜑 → ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = ((𝐼 · 𝐽) + (𝐾 · 𝑍)))
27	26, 13	eqtrd 2796	. . . . 5 ⊢ (𝜑 → ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1)
28	22, 27	jca 521	. . . 4 ⊢ (𝜑 → (((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1))
29		bezoutr1 16724	. . . . 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 43119	. 2 ⊢ (𝜑 → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)):(𝑅 PrimRoots 𝐾)⟶(𝑅 PrimRoots 𝐾))
33	1	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚)))
34		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = 𝑥) → 𝑚 = 𝑥)
35	34	oveq2d 7428	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = 𝑥) → (𝐼(.g‘𝑅)𝑚) = (𝐼(.g‘𝑅)𝑥))
36		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑥 ∈ (𝑅 PrimRoots 𝐾))
37	2	cmnmndd 19998	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Mnd)
38	37	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ Mnd)
39	4	nnnn0d 12648	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ ℕ0)
40	39	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐼 ∈ ℕ0)
41	3	nnnn0d 12648	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
42		eqid 2761	. . . . . . . . . . 11 ⊢ (.g‘𝑅) = (.g‘𝑅)
43	2, 41, 42	isprimroot 43111	. . . . . . . . . 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 2761	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
48	47, 42	mulgnn0cl 19280	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ ℕ0 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐼(.g‘𝑅)𝑥) ∈ (Base‘𝑅))
49	38, 40, 46, 48	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)𝑥) ∈ (Base‘𝑅))
50	33, 35, 36, 49	fvmptd 6993	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘𝑥) = (𝐼(.g‘𝑅)𝑥))
51	50	fveq2d 6881	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)))
52		eqidd 2762	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)) = (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)))
53		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = (𝐼(.g‘𝑅)𝑥)) → 𝑛 = (𝐼(.g‘𝑅)𝑥))
54	53	oveq2d 7428	. . . . . 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 2761	. . . . . . 7 ⊢ {𝑠 ∈ (Base‘𝑅) ∣ ∃𝑡 ∈ (Base‘𝑅)(𝑡(+g‘𝑅)𝑠) = (0g‘𝑅)} = {𝑠 ∈ (Base‘𝑅) ∣ ∃𝑡 ∈ (Base‘𝑅)(𝑡(+g‘𝑅)𝑠) = (0g‘𝑅)}
60	55, 56, 57, 58, 36, 59	primrootscoprmpow 43117	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)𝑥) ∈ (𝑅 PrimRoots 𝐾))
61	7	nnnn0d 12648	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℕ0)
62	61	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐽 ∈ ℕ0)
63	47, 42	mulgnn0cl 19280	. . . . . . 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 6993	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
66	62, 40, 46	3jca 1146	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝑥 ∈ (Base‘𝑅)))
67	47, 42	mulgnn0ass 19300	. . . . . . 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 43116	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))
71	70	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
72	71	eleq2d 2847	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) ↔ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
73	72	biimpd 232	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) → 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
74	70	simprd 501	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Abel)
75		ablgrp 19979	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ↾s 𝑈) ∈ Abel → (𝑅 ↾s 𝑈) ∈ Grp)
76	74, 75	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Grp)
77		grpmnd 19131	. . . . . . . . . . . . . . . . 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 2847	. . . . . . . . . . . . . . . . . . . . 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 7420	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑓 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑓))
85	84	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑓 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
86	85	rexbidv 3187	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑓 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
87	86	elrab 3645	. . . . . . . . . . . . . . . . . . . . 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 3937	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑅))
93		oveq2 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (0g‘𝑅) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(0g‘𝑅)))
94	93	eqeq1d 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (0g‘𝑅) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
95	94	rexbidv 3187	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (0g‘𝑅) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
96		eqid 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0g‘𝑅) = (0g‘𝑅)
97	47, 96	mndidcl 18919	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ Mnd → (0g‘𝑅) ∈ (Base‘𝑅))
98	37, 97	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅))
99		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → 𝑖 = (0g‘𝑅))
100	99	oveq1d 7427	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → (𝑖(+g‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)))
101	100	eqeq1d 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → ((𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅) ↔ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
102		eqid 2761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (+g‘𝑅) = (+g‘𝑅)
103	47, 102, 96	mndlid 18924	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
104	37, 98, 103	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
105	98, 101, 104	rspcedvd 3579	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
106	95, 98, 105	elrabd 3647	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
107	80	eleq2d 2847	. . . . . . . . . . . . . . . . 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 18980	. . . . . . . . . . . . . 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 12653	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐽 · 𝐼) ∈ ℕ0)
117	74	ablcmnd 19982	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ CMnd)
118		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (.g‘(𝑅 ↾s 𝑈)) = (.g‘(𝑅 ↾s 𝑈))
119	117, 41, 118	isprimroot 43111	. . . . . . . . . . . . . . . 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 2761	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ↾s 𝑈) = (𝑅 ↾s 𝑈)
124	123, 47	ressbas2 17396	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ⊆ (Base‘𝑅) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
125	92, 124	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
126	125	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
127	126	eleq2d 2847	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))))
128	122, 127	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑥 ∈ 𝑈)
129	42, 123, 118	submmulg 19308	. . . . . . . . . . . 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 11310	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐼 · 𝐽) ∈ ℂ)
133	3	nncnd 12332	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ ℂ)
134	9	zcnd 12785	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑍 ∈ ℂ)
135	133, 134	mulcld 11310	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐾 · 𝑍) ∈ ℂ)
136		1cnd 11283	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 1 ∈ ℂ)
137	132, 135, 136	addlsub 11713	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1 ↔ (𝐼 · 𝐽) = (1 − (𝐾 · 𝑍))))
138	13, 137	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 − (𝐾 · 𝑍)))
139	133, 134	mulcomd 11311	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐾 · 𝑍) = (𝑍 · 𝐾))
140	139	oveq2d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 − (𝐾 · 𝑍)) = (1 − (𝑍 · 𝐾)))
141	138, 140	eqtrd 2796	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 − (𝑍 · 𝐾)))
142	139, 135	eqeltrrd 2862	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑍 · 𝐾) ∈ ℂ)
143	136, 142	negsubd 11656	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 + -(𝑍 · 𝐾)) = (1 − (𝑍 · 𝐾)))
144	143	eqcomd 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 − (𝑍 · 𝐾)) = (1 + -(𝑍 · 𝐾)))
145	141, 144	eqtrd 2796	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 + -(𝑍 · 𝐾)))
146	145	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐼 · 𝐽) = (1 + -(𝑍 · 𝐾)))
147	131, 146	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐽 · 𝐼) = (1 + -(𝑍 · 𝐾)))
148	147	oveq1d 7427	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥) = ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥))
149	76	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ Grp)
150		1zzd 12708	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 1 ∈ ℤ)
151	9	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑍 ∈ ℤ)
152	6	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐾 ∈ ℤ)
153	151, 152	zmulcld 12790	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍 · 𝐾) ∈ ℤ)
154	153	znegcld 12786	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → -(𝑍 · 𝐾) ∈ ℤ)
155	150, 154, 122	3jca 1146	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))))
156		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (Base‘(𝑅 ↾s 𝑈)) = (Base‘(𝑅 ↾s 𝑈))
157		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (+g‘(𝑅 ↾s 𝑈)) = (+g‘(𝑅 ↾s 𝑈))
158	156, 118, 157	mulgdir 19296	. . . . . . . . . . . . . 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 19271	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)) → (1(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
161	122, 160	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (1(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
162		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (invg‘(𝑅 ↾s 𝑈)) = (invg‘(𝑅 ↾s 𝑈))
163	156, 118, 162	mulgneg 19282	. . . . . . . . . . . . . . . 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 7430	. . . . . . . . . . . . . 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 19301	. . . . . . . . . . . . . . . . . . . 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 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)) = (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
171		eqid 2761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0g‘(𝑅 ↾s 𝑈)) = (0g‘(𝑅 ↾s 𝑈))
172	156, 118, 171	mulgz 19292	. . . . . . . . . . . . . . . . . . . . 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 2796	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)) = (0g‘(𝑅 ↾s 𝑈)))
175	168, 174	eqtrd 2796	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)))
176	175	fveq2d 6881	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))))
177	171, 162	grpinvid 19190	. . . . . . . . . . . . . . . . . . 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 2796	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = (0g‘(𝑅 ↾s 𝑈)))
181	180	oveq2d 7428	. . . . . . . . . . . . . . 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 18925	. . . . . . . . . . . . . . . 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 2796	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥(+g‘(𝑅 ↾s 𝑈))((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥))) = 𝑥)
186	165, 185	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = 𝑥)
187	159, 186	eqtrd 2796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
188	148, 187	eqtrd 2796	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
189	130, 188	eqtrd 2796	. . . . . . . . . 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 2798	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)) = 𝑥)
195	65, 194	eqtrd 2796	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)) = 𝑥)
196	51, 195	eqtrd 2796	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = 𝑥)
197	196	ralrimiva 3155	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (𝑅 PrimRoots 𝐾)((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = 𝑥)
198		eqidd 2762	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)) = (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)))
199		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = 𝑦) → 𝑛 = 𝑦)
200	199	oveq2d 7428	. . . . . 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 43111	. . . . . . . . . 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 19280	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐽 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐽(.g‘𝑅)𝑦) ∈ (Base‘𝑅))
209	202, 203, 207, 208	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)𝑦) ∈ (Base‘𝑅))
210	198, 200, 201, 209	fvmptd 6993	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦) = (𝐽(.g‘𝑅)𝑦))
211	210	fveq2d 6881	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = (𝐹‘(𝐽(.g‘𝑅)𝑦)))
212	1	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚)))
213		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = (𝐽(.g‘𝑅)𝑦)) → 𝑚 = (𝐽(.g‘𝑅)𝑦))
214	213	oveq2d 7428	. . . . . 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 43117	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)𝑦) ∈ (𝑅 PrimRoots 𝐾))
220	39	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐼 ∈ ℕ0)
221	47, 42	mulgnn0cl 19280	. . . . . . 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 6993	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘(𝐽(.g‘𝑅)𝑦)) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
224	220, 203, 207	3jca 1146	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 ∈ ℕ0 ∧ 𝐽 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑅)))
225	47, 42	mulgnn0ass 19300	. . . . . . 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 12653	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 · 𝐽) ∈ ℕ0)
229	128	ex 418	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → 𝑥 ∈ 𝑈))
230	229	ssrdv 3937	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ 𝑈)
231	71	sseq1d 3962	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) ⊆ 𝑈 ↔ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ 𝑈))
232	230, 231	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ 𝑈)
233	232	sseld 3930	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) → 𝑦 ∈ 𝑈))
234	233	imp 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ 𝑈)
235	42, 123, 118	submmulg 19308	. . . . . . . 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 7427	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦) = ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦))
239	76	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ Grp)
240		1zzd 12708	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 1 ∈ ℤ)
241	9	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑍 ∈ ℤ)
242	6	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℤ)
243	241, 242	zmulcld 12790	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍 · 𝐾) ∈ ℤ)
244	243	znegcld 12786	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → -(𝑍 · 𝐾) ∈ ℤ)
245	232, 125	sseqtrd 3967	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ (Base‘(𝑅 ↾s 𝑈)))
246	245	sseld 3930	. . . . . . . . . . . 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 19296	. . . . . . . . . 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 19271	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)) → (1(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
252	247, 251	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (1(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
253	156, 118, 162	mulgneg 19282	. . . . . . . . . . . . 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 19301	. . . . . . . . . . . . . . . 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 43111	. . . . . . . . . . . . . . . . . . . . . . 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 2847	. . . . . . . . . . . . . . . . . . . 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 7428	. . . . . . . . . . . . . . . 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 2796	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)) = (0g‘(𝑅 ↾s 𝑈)))
270	257, 269	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
271	270	fveq2d 6881	. . . . . . . . . . . . 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 2796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = (0g‘(𝑅 ↾s 𝑈)))
274	254, 273	eqtrd 2796	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
275	252, 274	oveq12d 7430	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = (𝑦(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
276	156, 157, 171, 239, 247	grpridd 19161	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑦(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = 𝑦)
277	275, 276	eqtrd 2796	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = 𝑦)
278	250, 277	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
279	238, 278	eqtrd 2796	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
280	236, 279	eqtrd 2796	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = 𝑦)
281	226, 280	eqtr3d 2798	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)) = 𝑦)
282	223, 281	eqtrd 2796	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘(𝐽(.g‘𝑅)𝑦)) = 𝑦)
283	211, 282	eqtrd 2796	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = 𝑦)
284	283	ralrimiva 3155	. 2 ⊢ (𝜑 → ∀𝑦 ∈ (𝑅 PrimRoots 𝐾)(𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = 𝑦)
285	18, 32, 197, 284	2fvidf1od 7298	1 ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)–1-1-onto→(𝑅 PrimRoots 𝐾))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087  {crab 3413   ⊆ wss 3899   class class class wbr 5103   ↦ cmpt 5186  –1-1-onto→wf1o 6530  ‘cfv 6531  (class class class)co 7412  ℂcc 11179  1c1 11182   + caddc 11184   · cmul 11186   − cmin 11522  -cneg 11523  ℕcn 12316  ℕ₀cn0 12587  ℤcz 12674   ∥ cdvds 16402   gcd cgcd 16644  Basecbs 17367   ↾_s cress 17388  +_gcplusg 17408  0_gc0g 17590  Mndcmnd 18903  SubMndcsubmnd 18957  Grpcgrp 19124  inv_gcminusg 19125  ._gcmg 19257  CMndccmn 19974  Abelcabl 19975   PrimRoots cprimroots 43109

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258  ax-pre-sup 11259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7867  df-1st 7990  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-sup 9418  df-inf 9419  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-div 11955  df-nn 12317  df-2 12386  df-3 12387  df-n0 12588  df-z 12675  df-uz 12947  df-rp 13102  df-fz 13621  df-fl 13912  df-mod 13990  df-seq 14125  df-exp 14185  df-cj 15246  df-re 15247  df-im 15248  df-sqrt 15382  df-abs 15383  df-dvds 16403  df-gcd 16645  df-sets 17322  df-slot 17340  df-ndx 17352  df-base 17368  df-ress 17389  df-plusg 17421  df-0g 17592  df-mgm 18796  df-sgrp 18888  df-mnd 18904  df-submnd 18959  df-grp 19127  df-minusg 19128  df-mulg 19258  df-cmn 19976  df-abl 19977  df-primroots 43110

This theorem is used by:  primrootscoprbij2  43121