Metamath Proof Explorer

Theorem aks6d1c1p3

Description: In a field with a Frobenius isomorphism (read: algebraic closure or finite field), N and linear factors are introspective. (Contributed by metakunt, 25-Apr-2025)

Ref Expression
Hypotheses aks6d1c1p3.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 ↑ 𝑦 ) ) ) }
aks6d1c1p3.2 ⊢ 𝑆 = ( Poly1 ‘ 𝐾 )
aks6d1c1p3.3 ⊢ 𝐵 = ( Base ‘ 𝑆 )
aks6d1c1p3.4 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
aks6d1c1p3.5 ⊢ 𝑊 = ( mulGrp ‘ 𝑆 )
aks6d1c1p3.6 ⊢ 𝑉 = ( mulGrp ‘ 𝐾 )
aks6d1c1p3.7 ⊢ ↑ = ( .g ‘ 𝑉 )
aks6d1c1p3.8 ⊢ 𝐶 = ( algSc ‘ 𝑆 )
aks6d1c1p3.9 ⊢ 𝐷 = ( .g ‘ 𝑊 )
aks6d1c1p3.10 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c1p3.11 ⊢ 𝑂 = ( eval1 ‘ 𝐾 )
aks6d1c1p3.12 ⊢ + = ( +g ‘ 𝑆 )
aks6d1c1p3.13 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1c1p3.14 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c1p3.15 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks6d1c1p3.16 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks6d1c1p3.17 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks6d1c1p3.18 ⊢ 𝐹 = ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
aks6d1c1p3.19 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
aks6d1c1p3.20 ⊢ ( 𝜑 → 𝑁 ∼ 𝐹 )
aks6d1c1p3.21 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
Assertion aks6d1c1p3 ( 𝜑 → ( 𝑁 / 𝑃 ) ∼ 𝐹 )

Proof

Step Hyp Ref Expression
1 aks6d1c1p3.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 ↑ 𝑦 ) ) ) }
2 aks6d1c1p3.2 ⊢ 𝑆 = ( Poly1 ‘ 𝐾 )
3 aks6d1c1p3.3 ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 aks6d1c1p3.4 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
5 aks6d1c1p3.5 ⊢ 𝑊 = ( mulGrp ‘ 𝑆 )
6 aks6d1c1p3.6 ⊢ 𝑉 = ( mulGrp ‘ 𝐾 )
7 aks6d1c1p3.7 ⊢ ↑ = ( .g ‘ 𝑉 )
8 aks6d1c1p3.8 ⊢ 𝐶 = ( algSc ‘ 𝑆 )
9 aks6d1c1p3.9 ⊢ 𝐷 = ( .g ‘ 𝑊 )
10 aks6d1c1p3.10 ⊢ 𝑃 = ( chr ‘ 𝐾 )
11 aks6d1c1p3.11 ⊢ 𝑂 = ( eval1 ‘ 𝐾 )
12 aks6d1c1p3.12 ⊢ + = ( +g ‘ 𝑆 )
13 aks6d1c1p3.13 ⊢ ( 𝜑 → 𝐾 ∈ Field )
14 aks6d1c1p3.14 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
15 aks6d1c1p3.15 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
16 aks6d1c1p3.16 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
17 aks6d1c1p3.17 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
18 aks6d1c1p3.18 ⊢ 𝐹 = ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
19 aks6d1c1p3.19 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
20 aks6d1c1p3.20 ⊢ ( 𝜑 → 𝑁 ∼ 𝐹 )
21 aks6d1c1p3.21 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
22 18 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐹 = ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
23 22 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑂 ‘ 𝐹 ) = ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
24 23 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) = ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) )
25 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
26 13 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐾 ∈ CRing )
28 eqid ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
29 6 crngmgp ⊢ ( 𝐾 ∈ CRing → 𝑉 ∈ CMnd )
30 26 29 syl ⊢ ( 𝜑 → 𝑉 ∈ CMnd )
31 30 cmnmndd ⊢ ( 𝜑 → 𝑉 ∈ Mnd )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑉 ∈ Mnd )
33 1 20 aks6d1c1p1rcl ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) )
34 33 simpld ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
35 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
36 14 35 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
37 nndivdvds ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℕ ) → ( 𝑃 ∥ 𝑁 ↔ ( 𝑁 / 𝑃 ) ∈ ℕ ) )
38 34 36 37 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∥ 𝑁 ↔ ( 𝑁 / 𝑃 ) ∈ ℕ ) )
39 17 38 mpbid ⊢ ( 𝜑 → ( 𝑁 / 𝑃 ) ∈ ℕ )
40 39 nnnn0d ⊢ ( 𝜑 → ( 𝑁 / 𝑃 ) ∈ ℕ0 )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑁 / 𝑃 ) ∈ ℕ0 )
42 15 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
43 30 42 7 isprimroot ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ↔ ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) ) )
44 43 biimpd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) ) )
45 44 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) )
46 45 simp1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝑉 ) )
47 28 7 32 41 46 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ∈ ( Base ‘ 𝑉 ) )
48 6 25 mgpbas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝑉 )
49 48 eqcomi ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝐾 )
50 49 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑉 ) = ( Base ‘ 𝐾 ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( Base ‘ 𝑉 ) = ( Base ‘ 𝐾 ) )
52 47 51 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
53 11 4 25 2 3 27 52 evl1vard ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) )
54 26 crngringd ⊢ ( 𝜑 → 𝐾 ∈ Ring )
55 eqid ⊢ ( ℤRHom ‘ 𝐾 ) = ( ℤRHom ‘ 𝐾 )
56 55 zrhrhm ⊢ ( 𝐾 ∈ Ring → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) )
57 rhmghm ⊢ ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring GrpHom 𝐾 ) )
58 zringbas ⊢ ℤ = ( Base ‘ ℤring )
59 58 25 ghmf ⊢ ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring GrpHom 𝐾 ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
60 54 56 57 59 4syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
61 60 19 ffvelcdmd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝐾 ) )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝐾 ) )
63 11 2 25 8 3 27 62 52 evl1scad ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
64 eqid ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
65 11 2 25 3 27 52 53 63 12 64 evl1addd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) = ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
66 65 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) = ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
67 24 66 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) = ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
68 23 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) = ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) )
69 68 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑁 / 𝑃 ) ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑁 / 𝑃 ) ↑ ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) ) )
70 51 eleq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ↔ 𝑦 ∈ ( Base ‘ 𝐾 ) ) )
71 46 70 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
72 11 4 49 2 3 27 46 evl1vard ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑦 ) = 𝑦 ) )
73 11 2 25 8 3 27 62 71 evl1scad ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ 𝑦 ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
74 11 2 25 3 27 71 72 73 12 64 evl1addd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) = ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
75 74 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) = ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
76 75 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑁 / 𝑃 ) ↑ ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) ) = ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
77 69 76 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑁 / 𝑃 ) ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
78 25 25 isrim ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ∈ ( 𝐾 RingHom 𝐾 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) )
79 21 78 sylib ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ∈ ( 𝐾 RingHom 𝐾 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) )
80 79 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
82 27 crnggrpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐾 ∈ Grp )
83 25 64 82 52 62 grpcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ ( Base ‘ 𝐾 ) )
84 f1ocnvfv1 ⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ∧ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) = ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
85 81 83 84 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) = ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
86 85 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) = ( ◡ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
87 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) )
88 id ⊢ ( 𝑥 = ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) → 𝑥 = ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
89 88 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) ∧ 𝑥 = ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) → 𝑥 = ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
90 89 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) ∧ 𝑥 = ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
91 eqid ⊢ ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
92 91 25 mgpbas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
93 6 fveq2i ⊢ ( .g ‘ 𝑉 ) = ( .g ‘ ( mulGrp ‘ 𝐾 ) )
94 7 93 eqtri ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐾 ) )
95 91 ringmgp ⊢ ( 𝐾 ∈ Ring → ( mulGrp ‘ 𝐾 ) ∈ Mnd )
96 54 95 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝐾 ) ∈ Mnd )
97 96 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( mulGrp ‘ 𝐾 ) ∈ Mnd )
98 36 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
99 98 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑃 ∈ ℕ0 )
100 92 94 97 99 83 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑃 ↑ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ ( Base ‘ 𝐾 ) )
101 87 90 83 100 fvmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( 𝑃 ↑ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
102 101 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑃 ↑ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
103 79 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ∈ ( 𝐾 RingHom 𝐾 ) )
104 rhmghm ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ∈ ( 𝐾 RingHom 𝐾 ) → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ∈ ( 𝐾 GrpHom 𝐾 ) )
105 103 104 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ∈ ( 𝐾 GrpHom 𝐾 ) )
106 105 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ∈ ( 𝐾 GrpHom 𝐾 ) )
107 25 64 64 ghmlin ⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ∈ ( 𝐾 GrpHom 𝐾 ) ∧ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) ( +g ‘ 𝐾 ) ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
108 106 52 62 107 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) ( +g ‘ 𝐾 ) ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
109 id ⊢ ( 𝑥 = ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) → 𝑥 = ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) )
110 109 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) ∧ 𝑥 = ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) → 𝑥 = ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) )
111 110 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) ∧ 𝑥 = ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) )
112 92 94 97 99 52 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) ∈ ( Base ‘ 𝐾 ) )
113 87 111 52 112 fvmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) = ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) )
114 id ⊢ ( 𝑥 = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) → 𝑥 = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) )
115 114 oveq2d ⊢ ( 𝑥 = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
116 115 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) ∧ 𝑥 = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
117 eqid ⊢ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 )
118 10 25 94 117 14 19 26 fermltlchr ⊢ ( 𝜑 → ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) )
119 118 eqcomd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) = ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
120 119 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) = ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
121 120 62 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ ( Base ‘ 𝐾 ) )
122 87 116 62 121 fvmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) = ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
123 113 122 oveq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) ( +g ‘ 𝐾 ) ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) ( +g ‘ 𝐾 ) ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
124 102 108 123 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑃 ↑ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) ( +g ‘ 𝐾 ) ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
125 34 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
126 125 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑁 ∈ ℂ )
127 36 nncnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
128 127 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑃 ∈ ℂ )
129 36 nnne0d ⊢ ( 𝜑 → 𝑃 ≠ 0 )
130 129 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑃 ≠ 0 )
131 126 128 130 divcan2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑃 · ( 𝑁 / 𝑃 ) ) = 𝑁 )
132 131 oveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( 𝑁 ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
133 68 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 𝑁 ↑ ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) ) )
134 75 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑁 ↑ ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑦 ) ) = ( 𝑁 ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
135 133 134 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 𝑁 ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
136 135 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑁 ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) )
137 fveq2 ⊢ ( 𝑧 = 𝑦 → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) = ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) )
138 137 oveq2d ⊢ ( 𝑧 = 𝑦 → ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) )
139 oveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑁 ↑ 𝑧 ) = ( 𝑁 ↑ 𝑦 ) )
140 139 fveq2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑦 ) ) )
141 138 140 eqeq12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑧 ) ) ↔ ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑦 ) ) ) )
142 2 ply1crng ⊢ ( 𝐾 ∈ CRing → 𝑆 ∈ CRing )
143 26 142 syl ⊢ ( 𝜑 → 𝑆 ∈ CRing )
144 143 crnggrpd ⊢ ( 𝜑 → 𝑆 ∈ Grp )
145 4 2 3 vr1cl ⊢ ( 𝐾 ∈ Ring → 𝑋 ∈ 𝐵 )
146 54 145 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
147 2 8 25 3 ply1sclcl ⊢ ( ( 𝐾 ∈ Ring ∧ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 )
148 54 61 147 syl2anc ⊢ ( 𝜑 → ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 )
149 144 146 148 3jca ⊢ ( 𝜑 → ( 𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 ) )
150 3 12 grpcl ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 ) → ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ 𝐵 )
151 149 150 syl ⊢ ( 𝜑 → ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ 𝐵 )
152 18 a1i ⊢ ( 𝜑 → 𝐹 = ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
153 152 eleq1d ⊢ ( 𝜑 → ( 𝐹 ∈ 𝐵 ↔ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ 𝐵 ) )
154 151 153 mpbird ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
155 1 154 34 aks6d1c1p1 ⊢ ( 𝜑 → ( 𝑁 ∼ 𝐹 ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑦 ) ) ) )
156 20 155 mpbid ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑦 ) ) )
157 fveq2 ⊢ ( 𝑦 = 𝑧 → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) = ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) )
158 157 oveq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) )
159 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑁 ↑ 𝑦 ) = ( 𝑁 ↑ 𝑧 ) )
160 159 fveq2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑧 ) ) )
161 158 160 eqeq12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑦 ) ) ↔ ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑧 ) ) ) )
162 161 cbvralvw ⊢ ( ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑧 ) ) )
163 156 162 sylib ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑧 ) ) )
164 163 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ∀ 𝑧 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑧 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑧 ) ) )
165 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) )
166 141 164 165 rspcdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑦 ) ) )
167 23 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑦 ) ) = ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ↑ 𝑦 ) ) )
168 34 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
169 168 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑁 ∈ ℕ0 )
170 28 7 32 169 46 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑁 ↑ 𝑦 ) ∈ ( Base ‘ 𝑉 ) )
171 170 51 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑁 ↑ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
172 146 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑋 ∈ 𝐵 )
173 11 4 25 2 3 27 171 evl1vard ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ ( 𝑁 ↑ 𝑦 ) ) = ( 𝑁 ↑ 𝑦 ) ) )
174 173 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝑋 ) ‘ ( 𝑁 ↑ 𝑦 ) ) = ( 𝑁 ↑ 𝑦 ) )
175 172 174 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ ( 𝑁 ↑ 𝑦 ) ) = ( 𝑁 ↑ 𝑦 ) ) )
176 148 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 )
177 11 2 25 8 3 27 62 171 evl1scad ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ ( 𝑁 ↑ 𝑦 ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
178 177 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ ( 𝑁 ↑ 𝑦 ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) )
179 176 178 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ ( 𝑁 ↑ 𝑦 ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
180 11 2 25 3 27 171 175 179 12 64 evl1addd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ↑ 𝑦 ) ) = ( ( 𝑁 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
181 180 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ ( 𝑋 + ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ↑ 𝑦 ) ) = ( ( 𝑁 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
182 167 181 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝑁 ↑ 𝑦 ) ) = ( ( 𝑁 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
183 166 182 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑁 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑁 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
184 136 183 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑁 ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( 𝑁 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
185 132 184 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( 𝑁 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
186 131 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑁 = ( 𝑃 · ( 𝑁 / 𝑃 ) ) )
187 186 oveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑁 ↑ 𝑦 ) = ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ 𝑦 ) )
188 187 120 oveq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑁 ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) = ( ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
189 185 188 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
190 71 92 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
191 99 41 190 3jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑃 ∈ ℕ0 ∧ ( 𝑁 / 𝑃 ) ∈ ℕ0 ∧ 𝑦 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ) )
192 eqid ⊢ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
193 192 94 mulgnn0ass ⊢ ( ( ( mulGrp ‘ 𝐾 ) ∈ Mnd ∧ ( 𝑃 ∈ ℕ0 ∧ ( 𝑁 / 𝑃 ) ∈ ℕ0 ∧ 𝑦 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ) ) → ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ 𝑦 ) = ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) )
194 97 191 193 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ 𝑦 ) = ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) )
195 194 oveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) ( +g ‘ 𝐾 ) ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
196 189 195 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) ( +g ‘ 𝐾 ) ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
197 25 64 82 71 62 grpcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ ( Base ‘ 𝐾 ) )
198 197 92 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
199 99 41 198 3jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑃 ∈ ℕ0 ∧ ( 𝑁 / 𝑃 ) ∈ ℕ0 ∧ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ) )
200 192 94 mulgnn0ass ⊢ ( ( ( mulGrp ‘ 𝐾 ) ∈ Mnd ∧ ( 𝑃 ∈ ℕ0 ∧ ( 𝑁 / 𝑃 ) ∈ ℕ0 ∧ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ) ) → ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
201 97 199 200 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
202 196 201 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) ( +g ‘ 𝐾 ) ( 𝑃 ↑ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
203 124 202 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑃 ↑ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
204 id ⊢ ( 𝑥 = ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) → 𝑥 = ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
205 204 oveq2d ⊢ ( 𝑥 = ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
206 205 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) ∧ 𝑥 = ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
207 92 94 97 41 197 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ ( Base ‘ 𝐾 ) )
208 203 100 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ∈ ( Base ‘ 𝐾 ) )
209 87 206 207 208 fvmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) = ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
210 209 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑃 ↑ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) = ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
211 101 203 210 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
212 211 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) = ( ◡ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ) )
213 f1ocnvfv1 ⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ∧ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ) = ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
214 81 207 213 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ↑ 𝑥 ) ) ‘ ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ) = ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
215 86 212 214 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) = ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
216 215 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑁 / 𝑃 ) ↑ ( 𝑦 ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
217 77 216 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) = ( ( 𝑁 / 𝑃 ) ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) )
218 67 217 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) = ( ( 𝑁 / 𝑃 ) ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) )
219 218 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑁 / 𝑃 ) ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) )
220 219 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( ( 𝑁 / 𝑃 ) ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) )
221 1 154 39 aks6d1c1p1 ⊢ ( 𝜑 → ( ( 𝑁 / 𝑃 ) ∼ 𝐹 ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( ( 𝑁 / 𝑃 ) ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( ( 𝑁 / 𝑃 ) ↑ 𝑦 ) ) ) )
222 220 221 mpbird ⊢ ( 𝜑 → ( 𝑁 / 𝑃 ) ∼ 𝐹 )