Theorem primrootscoprbij 42910

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 12635	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
6	3	nnzd 12635	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℤ)
7		primrootscoprbij.5	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℕ)
8	7	nnzd 12635	. . . . . . 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 2772	. . . . 5 ⊢ (𝜑 → ((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1)
14	11, 13	jca 521	. . . 4 ⊢ (𝜑 → (((𝐼 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1))
15		bezoutr1 16652	. . . . 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 42909	. 2 ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)⟶(𝑅 PrimRoots 𝐾))
19		eqid 2766	. . 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 12267	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℂ)
24	4	nncnd 12267	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ ℂ)
25	23, 24	mulcomd 11248	. . . . . . 7 ⊢ (𝜑 → (𝐽 · 𝐼) = (𝐼 · 𝐽))
26	25	oveq1d 7438	. . . . . 6 ⊢ (𝜑 → ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = ((𝐼 · 𝐽) + (𝐾 · 𝑍)))
27	26, 13	eqtrd 2801	. . . . 5 ⊢ (𝜑 → ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1)
28	22, 27	jca 521	. . . 4 ⊢ (𝜑 → (((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝐼 ∈ ℤ ∧ 𝑍 ∈ ℤ)) ∧ ((𝐽 · 𝐼) + (𝐾 · 𝑍)) = 1))
29		bezoutr1 16652	. . . . 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 42909	. 2 ⊢ (𝜑 → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)):(𝑅 PrimRoots 𝐾)⟶(𝑅 PrimRoots 𝐾))
33	1	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚)))
34		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = 𝑥) → 𝑚 = 𝑥)
35	34	oveq2d 7439	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = 𝑥) → (𝐼(.g‘𝑅)𝑚) = (𝐼(.g‘𝑅)𝑥))
36		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑥 ∈ (𝑅 PrimRoots 𝐾))
37	2	cmnmndd 19905	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Mnd)
38	37	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ Mnd)
39	4	nnnn0d 12583	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ ℕ0)
40	39	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐼 ∈ ℕ0)
41	3	nnnn0d 12583	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
42		eqid 2766	. . . . . . . . . . 11 ⊢ (.g‘𝑅) = (.g‘𝑅)
43	2, 41, 42	isprimroot 42901	. . . . . . . . . 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 2766	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
48	47, 42	mulgnn0cl 19187	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ ℕ0 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐼(.g‘𝑅)𝑥) ∈ (Base‘𝑅))
49	38, 40, 46, 48	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)𝑥) ∈ (Base‘𝑅))
50	33, 35, 36, 49	fvmptd 7004	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘𝑥) = (𝐼(.g‘𝑅)𝑥))
51	50	fveq2d 6892	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)))
52		eqidd 2767	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)) = (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)))
53		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = (𝐼(.g‘𝑅)𝑥)) → 𝑛 = (𝐼(.g‘𝑅)𝑥))
54	53	oveq2d 7439	. . . . . 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 2766	. . . . . . 7 ⊢ {𝑠 ∈ (Base‘𝑅) ∣ ∃𝑡 ∈ (Base‘𝑅)(𝑡(+g‘𝑅)𝑠) = (0g‘𝑅)} = {𝑠 ∈ (Base‘𝑅) ∣ ∃𝑡 ∈ (Base‘𝑅)(𝑡(+g‘𝑅)𝑠) = (0g‘𝑅)}
60	55, 56, 57, 58, 36, 59	primrootscoprmpow 42907	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)𝑥) ∈ (𝑅 PrimRoots 𝐾))
61	7	nnnn0d 12583	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℕ0)
62	61	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → 𝐽 ∈ ℕ0)
63	47, 42	mulgnn0cl 19187	. . . . . . 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 7004	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)) = (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)))
66	62, 40, 46	3jca 1146	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝑥 ∈ (Base‘𝑅)))
67	47, 42	mulgnn0ass 19207	. . . . . . 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 42906	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))
71	70	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
72	71	eleq2d 2852	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) ↔ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
73	72	biimpd 232	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑅 PrimRoots 𝐾) → 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
74	70	simprd 501	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Abel)
75		ablgrp 19886	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ↾s 𝑈) ∈ Abel → (𝑅 ↾s 𝑈) ∈ Grp)
76	74, 75	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Grp)
77		grpmnd 19038	. . . . . . . . . . . . . . . . 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 2852	. . . . . . . . . . . . . . . . . . . . 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 7431	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑓 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑓))
85	84	eqeq1d 2768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑓 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
86	85	rexbidv 3192	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑓 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
87	86	elrab 3653	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑓 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
88	87	biimpi 219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → (𝑓 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑓) = (0g‘𝑅)))
89	88	simpld 500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑓 ∈ (Base‘𝑅))
90	83, 89	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑈) → 𝑓 ∈ (Base‘𝑅))
91	90	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑓 ∈ 𝑈 → 𝑓 ∈ (Base‘𝑅)))
92	91	ssrdv 3946	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑅))
93		oveq2 7431	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (0g‘𝑅) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(0g‘𝑅)))
94	93	eqeq1d 2768	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (0g‘𝑅) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
95	94	rexbidv 3192	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (0g‘𝑅) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
96		eqid 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0g‘𝑅) = (0g‘𝑅)
97	47, 96	mndidcl 18836	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ Mnd → (0g‘𝑅) ∈ (Base‘𝑅))
98	37, 97	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅))
99		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → 𝑖 = (0g‘𝑅))
100	99	oveq1d 7438	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → (𝑖(+g‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)))
101	100	eqeq1d 2768	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → ((𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅) ↔ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
102		eqid 2766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (+g‘𝑅) = (+g‘𝑅)
103	47, 102, 96	mndlid 18841	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
104	37, 98, 103	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
105	98, 101, 104	rspcedvd 3586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
106	95, 98, 105	elrabd 3655	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
107	80	eleq2d 2852	. . . . . . . . . . . . . . . . 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 18894	. . . . . . . . . . . . . 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 12588	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐽 · 𝐼) ∈ ℕ0)
117	74	ablcmnd 19889	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ CMnd)
118		eqid 2766	. . . . . . . . . . . . . . . . 17 ⊢ (.g‘(𝑅 ↾s 𝑈)) = (.g‘(𝑅 ↾s 𝑈))
119	117, 41, 118	isprimroot 42901	. . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ↾s 𝑈) = (𝑅 ↾s 𝑈)
124	123, 47	ressbas2 17323	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ⊆ (Base‘𝑅) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
125	92, 124	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
126	125	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
127	126	eleq2d 2852	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))))
128	122, 127	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑥 ∈ 𝑈)
129	42, 123, 118	submmulg 19215	. . . . . . . . . . . 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 11247	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐼 · 𝐽) ∈ ℂ)
133	3	nncnd 12267	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ ℂ)
134	9	zcnd 12719	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑍 ∈ ℂ)
135	133, 134	mulcld 11247	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐾 · 𝑍) ∈ ℂ)
136		1cnd 11220	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 1 ∈ ℂ)
137	132, 135, 136	addlsub 11648	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝐼 · 𝐽) + (𝐾 · 𝑍)) = 1 ↔ (𝐼 · 𝐽) = (1 − (𝐾 · 𝑍))))
138	13, 137	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 − (𝐾 · 𝑍)))
139	133, 134	mulcomd 11248	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐾 · 𝑍) = (𝑍 · 𝐾))
140	139	oveq2d 7439	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 − (𝐾 · 𝑍)) = (1 − (𝑍 · 𝐾)))
141	138, 140	eqtrd 2801	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 − (𝑍 · 𝐾)))
142	139, 135	eqeltrrd 2867	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑍 · 𝐾) ∈ ℂ)
143	136, 142	negsubd 11593	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 + -(𝑍 · 𝐾)) = (1 − (𝑍 · 𝐾)))
144	143	eqcomd 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 − (𝑍 · 𝐾)) = (1 + -(𝑍 · 𝐾)))
145	141, 144	eqtrd 2801	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 · 𝐽) = (1 + -(𝑍 · 𝐾)))
146	145	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐼 · 𝐽) = (1 + -(𝑍 · 𝐾)))
147	131, 146	eqtrd 2801	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐽 · 𝐼) = (1 + -(𝑍 · 𝐾)))
148	147	oveq1d 7438	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥) = ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥))
149	76	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ Grp)
150		1zzd 12643	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 1 ∈ ℤ)
151	9	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑍 ∈ ℤ)
152	6	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐾 ∈ ℤ)
153	151, 152	zmulcld 12724	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍 · 𝐾) ∈ ℤ)
154	153	znegcld 12720	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → -(𝑍 · 𝐾) ∈ ℤ)
155	150, 154, 122	3jca 1146	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (1 ∈ ℤ ∧ -(𝑍 · 𝐾) ∈ ℤ ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑈))))
156		eqid 2766	. . . . . . . . . . . . . . 15 ⊢ (Base‘(𝑅 ↾s 𝑈)) = (Base‘(𝑅 ↾s 𝑈))
157		eqid 2766	. . . . . . . . . . . . . . 15 ⊢ (+g‘(𝑅 ↾s 𝑈)) = (+g‘(𝑅 ↾s 𝑈))
158	156, 118, 157	mulgdir 19203	. . . . . . . . . . . . . 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 19178	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (Base‘(𝑅 ↾s 𝑈)) → (1(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
161	122, 160	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (1(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
162		eqid 2766	. . . . . . . . . . . . . . . . 17 ⊢ (invg‘(𝑅 ↾s 𝑈)) = (invg‘(𝑅 ↾s 𝑈))
163	156, 118, 162	mulgneg 19189	. . . . . . . . . . . . . . . 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 7441	. . . . . . . . . . . . . 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 19208	. . . . . . . . . . . . . . . . . . . 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 7439	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)) = (𝑍(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
171		eqid 2766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0g‘(𝑅 ↾s 𝑈)) = (0g‘(𝑅 ↾s 𝑈))
172	156, 118, 171	mulgz 19199	. . . . . . . . . . . . . . . . . . . . 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 2801	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑥)) = (0g‘(𝑅 ↾s 𝑈)))
175	168, 174	eqtrd 2801	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥) = (0g‘(𝑅 ↾s 𝑈)))
176	175	fveq2d 6892	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = ((invg‘(𝑅 ↾s 𝑈))‘(0g‘(𝑅 ↾s 𝑈))))
177	171, 162	grpinvid 19097	. . . . . . . . . . . . . . . . . . 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 2801	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = (0g‘(𝑅 ↾s 𝑈)))
181	180	oveq2d 7439	. . . . . . . . . . . . . . 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 18842	. . . . . . . . . . . . . . . 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 2801	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑥(+g‘(𝑅 ↾s 𝑈))((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥))) = 𝑥)
186	165, 185	eqtrd 2801	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑥)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑥)) = 𝑥)
187	159, 186	eqtrd 2801	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
188	148, 187	eqtrd 2801	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ((𝐽 · 𝐼)(.g‘(𝑅 ↾s 𝑈))𝑥) = 𝑥)
189	130, 188	eqtrd 2801	. . . . . . . . . 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 2803	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)(𝐼(.g‘𝑅)𝑥)) = 𝑥)
195	65, 194	eqtrd 2801	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐼(.g‘𝑅)𝑥)) = 𝑥)
196	51, 195	eqtrd 2801	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = 𝑥)
197	196	ralrimiva 3160	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (𝑅 PrimRoots 𝐾)((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘(𝐹‘𝑥)) = 𝑥)
198		eqidd 2767	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)) = (𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛)))
199		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑛 = 𝑦) → 𝑛 = 𝑦)
200	199	oveq2d 7439	. . . . . 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 42901	. . . . . . . . . 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 19187	. . . . . . 7 ⊢ ((𝑅 ∈ Mnd ∧ 𝐽 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐽(.g‘𝑅)𝑦) ∈ (Base‘𝑅))
209	202, 203, 207, 208	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)𝑦) ∈ (Base‘𝑅))
210	198, 200, 201, 209	fvmptd 7004	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦) = (𝐽(.g‘𝑅)𝑦))
211	210	fveq2d 6892	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = (𝐹‘(𝐽(.g‘𝑅)𝑦)))
212	1	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚)))
213		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑚 = (𝐽(.g‘𝑅)𝑦)) → 𝑚 = (𝐽(.g‘𝑅)𝑦))
214	213	oveq2d 7439	. . . . . 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 42907	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐽(.g‘𝑅)𝑦) ∈ (𝑅 PrimRoots 𝐾))
220	39	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐼 ∈ ℕ0)
221	47, 42	mulgnn0cl 19187	. . . . . . 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 7004	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘(𝐽(.g‘𝑅)𝑦)) = (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)))
224	220, 203, 207	3jca 1146	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 ∈ ℕ0 ∧ 𝐽 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑅)))
225	47, 42	mulgnn0ass 19207	. . . . . . 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 12588	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼 · 𝐽) ∈ ℕ0)
229	128	ex 418	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → 𝑥 ∈ 𝑈))
230	229	ssrdv 3946	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ 𝑈)
231	71	sseq1d 3971	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) ⊆ 𝑈 ↔ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ 𝑈))
232	230, 231	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ 𝑈)
233	232	sseld 3939	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝑅 PrimRoots 𝐾) → 𝑦 ∈ 𝑈))
234	233	imp 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑦 ∈ 𝑈)
235	42, 123, 118	submmulg 19215	. . . . . . . 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 7438	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦) = ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦))
239	76	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ Grp)
240		1zzd 12643	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 1 ∈ ℤ)
241	9	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝑍 ∈ ℤ)
242	6	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℤ)
243	241, 242	zmulcld 12724	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍 · 𝐾) ∈ ℤ)
244	243	znegcld 12720	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → -(𝑍 · 𝐾) ∈ ℤ)
245	232, 125	sseqtrd 3976	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ (Base‘(𝑅 ↾s 𝑈)))
246	245	sseld 3939	. . . . . . . . . . . 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 19203	. . . . . . . . . 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 19178	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (Base‘(𝑅 ↾s 𝑈)) → (1(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
252	247, 251	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (1(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
253	156, 118, 162	mulgneg 19189	. . . . . . . . . . . . 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 19208	. . . . . . . . . . . . . . . 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 42901	. . . . . . . . . . . . . . . . . . . . . . 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 2852	. . . . . . . . . . . . . . . . . . . 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 7439	. . . . . . . . . . . . . . . 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 2801	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑍(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑦)) = (0g‘(𝑅 ↾s 𝑈)))
270	257, 269	eqtrd 2801	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
271	270	fveq2d 6892	. . . . . . . . . . . . 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 2801	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((invg‘(𝑅 ↾s 𝑈))‘((𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = (0g‘(𝑅 ↾s 𝑈)))
274	254, 273	eqtrd 2801	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦) = (0g‘(𝑅 ↾s 𝑈)))
275	252, 274	oveq12d 7441	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = (𝑦(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))))
276	156, 157, 171, 239, 247	grpridd 19068	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝑦(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = 𝑦)
277	275, 276	eqtrd 2801	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1(.g‘(𝑅 ↾s 𝑈))𝑦)(+g‘(𝑅 ↾s 𝑈))(-(𝑍 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑦)) = 𝑦)
278	250, 277	eqtrd 2801	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((1 + -(𝑍 · 𝐾))(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
279	238, 278	eqtrd 2801	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘(𝑅 ↾s 𝑈))𝑦) = 𝑦)
280	236, 279	eqtrd 2801	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐼 · 𝐽)(.g‘𝑅)𝑦) = 𝑦)
281	226, 280	eqtr3d 2803	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐼(.g‘𝑅)(𝐽(.g‘𝑅)𝑦)) = 𝑦)
282	223, 281	eqtrd 2801	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘(𝐽(.g‘𝑅)𝑦)) = 𝑦)
283	211, 282	eqtrd 2801	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅 PrimRoots 𝐾)) → (𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = 𝑦)
284	283	ralrimiva 3160	. 2 ⊢ (𝜑 → ∀𝑦 ∈ (𝑅 PrimRoots 𝐾)(𝐹‘((𝑛 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐽(.g‘𝑅)𝑛))‘𝑦)) = 𝑦)
285	18, 32, 197, 284	2fvidf1od 7307	1 ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)–1-1-onto→(𝑅 PrimRoots 𝐾))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ∀wral 3082  ∃wrex 3092  {crab 3419   ⊆ wss 3908   class class class wbr 5114   ↦ cmpt 5197  –1-1-onto→wf1o 6542  ‘cfv 6543  (class class class)co 7423  ℂcc 11116  1c1 11119   + caddc 11121   · cmul 11123   − cmin 11459  -cneg 11460  ℕcn 12251  ℕ₀cn0 12522  ℤcz 12609   ∥ cdvds 16335   gcd cgcd 16577  Basecbs 17294   ↾_s cress 17315  +_gcplusg 17335  0_gc0g 17517  Mndcmnd 18821  SubMndcsubmnd 18871  Grpcgrp 19031  inv_gcminusg 19032  ._gcmg 19164  CMndccmn 19881  Abelcabl 19882   PrimRoots cprimroots 42899

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195  ax-pre-sup 11196

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-1st 7995  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-sup 9412  df-inf 9413  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-div 11890  df-nn 12252  df-2 12321  df-3 12322  df-n0 12523  df-z 12610  df-uz 12881  df-rp 13035  df-fz 13554  df-fl 13845  df-mod 13923  df-seq 14058  df-exp 14118  df-cj 15176  df-re 15177  df-im 15178  df-sqrt 15312  df-abs 15313  df-dvds 16336  df-gcd 16578  df-sets 17249  df-slot 17267  df-ndx 17279  df-base 17295  df-ress 17316  df-plusg 17348  df-0g 17519  df-mgm 18723  df-sgrp 18806  df-mnd 18822  df-submnd 18873  df-grp 19034  df-minusg 19035  df-mulg 19165  df-cmn 19883  df-abl 19884  df-primroots 42900

This theorem is used by:  primrootscoprbij2  42911