Metamath Proof Explorer

Theorem aks6d1c2lem3

Description: Lemma for aks6d1c2 to simplify context. (Contributed by metakunt, 1-May-2025)

Ref Expression
Hypotheses aks6d1c2.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
aks6d1c2.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c2.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1c2.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c2.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks6d1c2.6 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks6d1c2.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks6d1c2.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks6d1c2.9 ⊢ ( 𝜑 → 𝐹 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
aks6d1c2.10 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
aks6d1c2.11 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
aks6d1c2.12 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
aks6d1c2.13 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
aks6d1c2.14 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
aks6d1c2.15 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
aks6d1c2.16 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
aks6d1c2.17 ⊢ 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) )
aks6d1c2.18 ⊢ 𝐵 = ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
aks6d1c2.19 ⊢ 𝐶 = ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) )
aks6d1c2.20 ⊢ ( 𝜑 → 𝐼 ∈ 𝐶 )
aks6d1c2.21 ⊢ ( 𝜑 → 𝐽 ∈ 𝐶 )
aks6d1c2.22 ⊢ ( 𝜑 → 𝐼 < 𝐽 )
aks6d1c2.23 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
aks6d1c2.24 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
aks6d1c2.25 ⊢ 𝑆 = ( ( 𝐽 ↑ 𝑋 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐼 ↑ 𝑋 ) )
aks6d1c2.26 ⊢ ( 𝜑 → 𝑈 ∈ ℕ )
aks6d1c2.27 ⊢ ( 𝜑 → 𝐽 = ( 𝐼 + ( 𝑈 · 𝑅 ) ) )
aks6d1c2p3.1 ⊢ ( 𝜑 → 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
aks6d1c2p3.2 ⊢ ( 𝜑 → 𝑟 ∈ ( 0 ... 𝐵 ) )
aks6d1c2p3.3 ⊢ ( 𝜑 → 𝑜 ∈ ( 0 ... 𝐵 ) )
aks6d1c2p3.4 ⊢ ( 𝜑 → 𝐽 = ( 𝑟 𝐸 𝑜 ) )
aks6d1c2p3.5 ⊢ ( 𝜑 → 𝑝 ∈ ( 0 ... 𝐵 ) )
aks6d1c2p3.6 ⊢ ( 𝜑 → 𝑞 ∈ ( 0 ... 𝐵 ) )
aks6d1c2p3.7 ⊢ ( 𝜑 → 𝐼 = ( 𝑝 𝐸 𝑞 ) )
aks6d1c2p3.8 ⊢ ( 𝜑 → 𝐼 ∈ ℕ0 )
Assertion aks6d1c2lem3 ( 𝜑 → ( 𝐽 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) = ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c2.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
2 aks6d1c2.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
3 aks6d1c2.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
4 aks6d1c2.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 aks6d1c2.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
6 aks6d1c2.6 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7 aks6d1c2.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
8 aks6d1c2.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
9 aks6d1c2.9 ⊢ ( 𝜑 → 𝐹 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
10 aks6d1c2.10 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
11 aks6d1c2.11 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
12 aks6d1c2.12 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
13 aks6d1c2.13 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
14 aks6d1c2.14 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
15 aks6d1c2.15 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
16 aks6d1c2.16 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
17 aks6d1c2.17 ⊢ 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) )
18 aks6d1c2.18 ⊢ 𝐵 = ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
19 aks6d1c2.19 ⊢ 𝐶 = ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) )
20 aks6d1c2.20 ⊢ ( 𝜑 → 𝐼 ∈ 𝐶 )
21 aks6d1c2.21 ⊢ ( 𝜑 → 𝐽 ∈ 𝐶 )
22 aks6d1c2.22 ⊢ ( 𝜑 → 𝐼 < 𝐽 )
23 aks6d1c2.23 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
24 aks6d1c2.24 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
25 aks6d1c2.25 ⊢ 𝑆 = ( ( 𝐽 ↑ 𝑋 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐼 ↑ 𝑋 ) )
26 aks6d1c2.26 ⊢ ( 𝜑 → 𝑈 ∈ ℕ )
27 aks6d1c2.27 ⊢ ( 𝜑 → 𝐽 = ( 𝐼 + ( 𝑈 · 𝑅 ) ) )
28 aks6d1c2p3.1 ⊢ ( 𝜑 → 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
29 aks6d1c2p3.2 ⊢ ( 𝜑 → 𝑟 ∈ ( 0 ... 𝐵 ) )
30 aks6d1c2p3.3 ⊢ ( 𝜑 → 𝑜 ∈ ( 0 ... 𝐵 ) )
31 aks6d1c2p3.4 ⊢ ( 𝜑 → 𝐽 = ( 𝑟 𝐸 𝑜 ) )
32 aks6d1c2p3.5 ⊢ ( 𝜑 → 𝑝 ∈ ( 0 ... 𝐵 ) )
33 aks6d1c2p3.6 ⊢ ( 𝜑 → 𝑞 ∈ ( 0 ... 𝐵 ) )
34 aks6d1c2p3.7 ⊢ ( 𝜑 → 𝐼 = ( 𝑝 𝐸 𝑞 ) )
35 aks6d1c2p3.8 ⊢ ( 𝜑 → 𝐼 ∈ ℕ0 )
36 12 a1i ⊢ ( 𝜑 → 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) )
37 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝑟 ∧ 𝑙 = 𝑜 ) ) → 𝑘 = 𝑟 )
38 37 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝑟 ∧ 𝑙 = 𝑜 ) ) → ( 𝑃 ↑ 𝑘 ) = ( 𝑃 ↑ 𝑟 ) )
39 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝑟 ∧ 𝑙 = 𝑜 ) ) → 𝑙 = 𝑜 )
40 39 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝑟 ∧ 𝑙 = 𝑜 ) ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) )
41 38 40 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝑟 ∧ 𝑙 = 𝑜 ) ) → ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) = ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) )
42 elfznn0 ⊢ ( 𝑟 ∈ ( 0 ... 𝐵 ) → 𝑟 ∈ ℕ0 )
43 29 42 syl ⊢ ( 𝜑 → 𝑟 ∈ ℕ0 )
44 elfznn0 ⊢ ( 𝑜 ∈ ( 0 ... 𝐵 ) → 𝑜 ∈ ℕ0 )
45 30 44 syl ⊢ ( 𝜑 → 𝑜 ∈ ℕ0 )
46 ovexd ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ∈ V )
47 36 41 43 45 46 ovmpod ⊢ ( 𝜑 → ( 𝑟 𝐸 𝑜 ) = ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) )
48 31 47 eqtrd ⊢ ( 𝜑 → 𝐽 = ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) )
49 48 oveq1d ⊢ ( 𝜑 → ( 𝐽 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) = ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) )
50 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝑝 ∧ 𝑙 = 𝑞 ) ) → 𝑘 = 𝑝 )
51 50 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝑝 ∧ 𝑙 = 𝑞 ) ) → ( 𝑃 ↑ 𝑘 ) = ( 𝑃 ↑ 𝑝 ) )
52 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝑝 ∧ 𝑙 = 𝑞 ) ) → 𝑙 = 𝑞 )
53 52 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝑝 ∧ 𝑙 = 𝑞 ) ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) )
54 51 53 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝑝 ∧ 𝑙 = 𝑞 ) ) → ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) = ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) )
55 elfznn0 ⊢ ( 𝑝 ∈ ( 0 ... 𝐵 ) → 𝑝 ∈ ℕ0 )
56 32 55 syl ⊢ ( 𝜑 → 𝑝 ∈ ℕ0 )
57 elfznn0 ⊢ ( 𝑞 ∈ ( 0 ... 𝐵 ) → 𝑞 ∈ ℕ0 )
58 33 57 syl ⊢ ( 𝜑 → 𝑞 ∈ ℕ0 )
59 ovexd ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ∈ V )
60 36 54 56 58 59 ovmpod ⊢ ( 𝜑 → ( 𝑝 𝐸 𝑞 ) = ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) )
61 34 60 eqtrd ⊢ ( 𝜑 → 𝐼 = ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) )
62 61 oveq1d ⊢ ( 𝜑 → ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) = ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) )
63 fveq2 ⊢ ( 𝑦 = 𝑀 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑦 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) )
64 63 oveq2d ⊢ ( 𝑦 = 𝑀 → ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑦 ) ) = ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) )
65 oveq2 ⊢ ( 𝑦 = 𝑀 → ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) = ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
66 65 fveq2d ⊢ ( 𝑦 = 𝑀 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
67 64 66 eqeq12d ⊢ ( 𝑦 = 𝑀 → ( ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ↔ ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ) )
68 nn0ex ⊢ ℕ0 ∈ V
69 68 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
70 ovexd ⊢ ( 𝜑 → ( 0 ... 𝐴 ) ∈ V )
71 elmapg ⊢ ( ( ℕ0 ∈ V ∧ ( 0 ... 𝐴 ) ∈ V ) → ( 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑠 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
72 69 70 71 syl2anc ⊢ ( 𝜑 → ( 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑠 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
73 28 72 mpbid ⊢ ( 𝜑 → 𝑠 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
74 eqid ⊢ ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) = ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) )
75 1 2 3 4 5 6 7 8 73 10 11 56 58 74 14 15 aks6d1c1rh ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ∼ ( 𝐺 ‘ 𝑠 ) )
76 1 75 aks6d1c1p1rcl ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ∈ ℕ ∧ ( 𝐺 ‘ 𝑠 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) )
77 76 simprd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑠 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
78 76 simpld ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ∈ ℕ )
79 1 77 78 aks6d1c1p1 ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ∼ ( 𝐺 ‘ 𝑠 ) ↔ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) )
80 75 79 mpbid ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) )
81 67 80 16 rspcdva ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
82 61 eqcomd ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) = 𝐼 )
83 82 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
84 48 eqcomd ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) = 𝐽 )
85 84 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 𝐽 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
86 27 oveq1d ⊢ ( 𝜑 → ( 𝐽 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( ( 𝐼 + ( 𝑈 · 𝑅 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
87 3 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
88 crngring ⊢ ( 𝐾 ∈ CRing → 𝐾 ∈ Ring )
89 87 88 syl ⊢ ( 𝜑 → 𝐾 ∈ Ring )
90 eqid ⊢ ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
91 90 ringmgp ⊢ ( 𝐾 ∈ Ring → ( mulGrp ‘ 𝐾 ) ∈ Mnd )
92 89 91 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝐾 ) ∈ Mnd )
93 26 nnnn0d ⊢ ( 𝜑 → 𝑈 ∈ ℕ0 )
94 5 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
95 93 94 nn0mulcld ⊢ ( 𝜑 → ( 𝑈 · 𝑅 ) ∈ ℕ0 )
96 90 crngmgp ⊢ ( 𝐾 ∈ CRing → ( mulGrp ‘ 𝐾 ) ∈ CMnd )
97 87 96 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝐾 ) ∈ CMnd )
98 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝐾 ) ) = ( .g ‘ ( mulGrp ‘ 𝐾 ) )
99 97 94 98 isprimroot ⊢ ( 𝜑 → ( 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ↔ ( 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ∀ 𝑣 ∈ ℕ0 ( ( 𝑣 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) → 𝑅 ∥ 𝑣 ) ) ) )
100 99 biimpd ⊢ ( 𝜑 → ( 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) → ( 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ∀ 𝑣 ∈ ℕ0 ( ( 𝑣 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) → 𝑅 ∥ 𝑣 ) ) ) )
101 16 100 mpd ⊢ ( 𝜑 → ( 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ∀ 𝑣 ∈ ℕ0 ( ( 𝑣 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) → 𝑅 ∥ 𝑣 ) ) )
102 101 simp1d ⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
103 35 95 102 3jca ⊢ ( 𝜑 → ( 𝐼 ∈ ℕ0 ∧ ( 𝑈 · 𝑅 ) ∈ ℕ0 ∧ 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ) )
104 eqid ⊢ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
105 eqid ⊢ ( +g ‘ ( mulGrp ‘ 𝐾 ) ) = ( +g ‘ ( mulGrp ‘ 𝐾 ) )
106 104 98 105 mulgnn0dir ⊢ ( ( ( mulGrp ‘ 𝐾 ) ∈ Mnd ∧ ( 𝐼 ∈ ℕ0 ∧ ( 𝑈 · 𝑅 ) ∈ ℕ0 ∧ 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ) ) → ( ( 𝐼 + ( 𝑈 · 𝑅 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( 𝑈 · 𝑅 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
107 92 103 106 syl2anc ⊢ ( 𝜑 → ( ( 𝐼 + ( 𝑈 · 𝑅 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( 𝑈 · 𝑅 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
108 93 94 102 3jca ⊢ ( 𝜑 → ( 𝑈 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ) )
109 104 98 mulgnn0ass ⊢ ( ( ( mulGrp ‘ 𝐾 ) ∈ Mnd ∧ ( 𝑈 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ) ) → ( ( 𝑈 · 𝑅 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 𝑈 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
110 92 108 109 syl2anc ⊢ ( 𝜑 → ( ( 𝑈 · 𝑅 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 𝑈 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
111 101 simp2d ⊢ ( 𝜑 → ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) )
112 111 oveq2d ⊢ ( 𝜑 → ( 𝑈 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( 𝑈 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ) )
113 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) )
114 104 98 113 mulgnn0z ⊢ ( ( ( mulGrp ‘ 𝐾 ) ∈ Mnd ∧ 𝑈 ∈ ℕ0 ) → ( 𝑈 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) )
115 92 93 114 syl2anc ⊢ ( 𝜑 → ( 𝑈 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) )
116 112 115 eqtrd ⊢ ( 𝜑 → ( 𝑈 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) )
117 110 116 eqtrd ⊢ ( 𝜑 → ( ( 𝑈 · 𝑅 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) )
118 117 oveq2d ⊢ ( 𝜑 → ( ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( 𝑈 · 𝑅 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ) )
119 104 98 92 35 102 mulgnn0cld ⊢ ( 𝜑 → ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
120 104 105 113 mndrid ⊢ ( ( ( mulGrp ‘ 𝐾 ) ∈ Mnd ∧ ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ) → ( ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ) = ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
121 92 119 120 syl2anc ⊢ ( 𝜑 → ( ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ) = ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
122 118 121 eqtrd ⊢ ( 𝜑 → ( ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( 𝑈 · 𝑅 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
123 107 122 eqtrd ⊢ ( 𝜑 → ( ( 𝐼 + ( 𝑈 · 𝑅 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
124 86 123 eqtrd ⊢ ( 𝜑 → ( 𝐽 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
125 85 124 eqtr2d ⊢ ( 𝜑 → ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
126 83 125 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
127 126 fveq2d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
128 63 oveq2d ⊢ ( 𝑦 = 𝑀 → ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑦 ) ) = ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) )
129 oveq2 ⊢ ( 𝑦 = 𝑀 → ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) = ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
130 129 fveq2d ⊢ ( 𝑦 = 𝑀 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
131 128 130 eqeq12d ⊢ ( 𝑦 = 𝑀 → ( ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ↔ ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ) )
132 eqid ⊢ ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) = ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) )
133 1 2 3 4 5 6 7 8 73 10 11 43 45 132 14 15 aks6d1c1rh ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ∼ ( 𝐺 ‘ 𝑠 ) )
134 1 133 aks6d1c1p1rcl ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ∈ ℕ ∧ ( 𝐺 ‘ 𝑠 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) )
135 134 simpld ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ∈ ℕ )
136 1 77 135 aks6d1c1p1 ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ∼ ( 𝐺 ‘ 𝑠 ) ↔ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) )
137 133 136 mpbid ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) )
138 131 137 16 rspcdva ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
139 138 eqcomd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) )
140 127 139 eqtrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) )
141 81 140 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑝 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑞 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) = ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) )
142 62 141 eqtr2d ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑟 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑜 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) = ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) )
143 49 142 eqtrd ⊢ ( 𝜑 → ( 𝐽 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) = ( 𝐼 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑠 ) ) ‘ 𝑀 ) ) )