Metamath Proof Explorer

Theorem primrootscoprbij

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

Ref Expression
Hypotheses 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 primrootscoprbij ( 𝜑 → 𝐹 : ( 𝑅 PrimRoots 𝐾 ) –1-1-onto→ ( 𝑅 PrimRoots 𝐾 ) )

Proof

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