Metamath Proof Explorer

Theorem aks6d1c6lem2

Description: Every primitive root is root of G(u)-G(v). (Contributed by metakunt, 8-May-2025)

Ref Expression
Hypotheses aks6d1c6.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
aks6d1c6.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c6.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1c6.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c6.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks6d1c6.6 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks6d1c6.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks6d1c6.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks6d1c6.9 ⊢ ( 𝜑 → 𝐴 < 𝑃 )
aks6d1c6.10 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
aks6d1c6.11 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
aks6d1c6.12 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
aks6d1c6.13 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
aks6d1c6.14 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
aks6d1c6.15 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
aks6d1c6.16 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
aks6d1c6.17 ⊢ 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) )
aks6d1c6.18 ⊢ 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
aks6d1c6.19 ⊢ 𝑆 = { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) }
aks6d1c6lem2.1 ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
aks6d1c6lem2.2 ⊢ ( 𝜑 → 𝑉 ∈ 𝑆 )
aks6d1c6lem2.3 ⊢ ( 𝜑 → ( ( 𝐻 ↾ 𝑆 ) ‘ 𝑈 ) = ( ( 𝐻 ↾ 𝑆 ) ‘ 𝑉 ) )
aks6d1c6lem2.4 ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
aks6d1c6lem2.5 ⊢ 𝐽 = ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
aks6d1c6lem2.6 ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≤ ( ♯ ‘ ( 𝐽 “ ( ℕ0 × ℕ0 ) ) ) )
Assertion aks6d1c6lem2 ( 𝜑 → 𝐷 ≤ ( ♯ ‘ ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c6.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
2 aks6d1c6.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
3 aks6d1c6.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
4 aks6d1c6.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 aks6d1c6.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
6 aks6d1c6.6 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7 aks6d1c6.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
8 aks6d1c6.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
9 aks6d1c6.9 ⊢ ( 𝜑 → 𝐴 < 𝑃 )
10 aks6d1c6.10 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
11 aks6d1c6.11 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
12 aks6d1c6.12 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
13 aks6d1c6.13 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
14 aks6d1c6.14 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
15 aks6d1c6.15 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
16 aks6d1c6.16 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
17 aks6d1c6.17 ⊢ 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) )
18 aks6d1c6.18 ⊢ 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
19 aks6d1c6.19 ⊢ 𝑆 = { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) }
20 aks6d1c6lem2.1 ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
21 aks6d1c6lem2.2 ⊢ ( 𝜑 → 𝑉 ∈ 𝑆 )
22 aks6d1c6lem2.3 ⊢ ( 𝜑 → ( ( 𝐻 ↾ 𝑆 ) ‘ 𝑈 ) = ( ( 𝐻 ↾ 𝑆 ) ‘ 𝑉 ) )
23 aks6d1c6lem2.4 ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
24 aks6d1c6lem2.5 ⊢ 𝐽 = ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
25 aks6d1c6lem2.6 ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≤ ( ♯ ‘ ( 𝐽 “ ( ℕ0 × ℕ0 ) ) ) )
26 fvexd ⊢ ( 𝜑 → ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ∈ V )
27 13 26 eqeltrid ⊢ ( 𝜑 → 𝐿 ∈ V )
28 27 imaexd ⊢ ( 𝜑 → ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∈ V )
29 hashxrcl ⊢ ( ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∈ V → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℝ* )
30 28 29 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℝ* )
31 18 30 eqeltrid ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
32 24 a1i ⊢ ( 𝜑 → 𝐽 = ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
33 nn0ex ⊢ ℕ0 ∈ V
34 33 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
35 34 34 xpexd ⊢ ( 𝜑 → ( ℕ0 × ℕ0 ) ∈ V )
36 35 mptexd ⊢ ( 𝜑 → ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ∈ V )
37 32 36 eqeltrd ⊢ ( 𝜑 → 𝐽 ∈ V )
38 37 imaexd ⊢ ( 𝜑 → ( 𝐽 “ ( ℕ0 × ℕ0 ) ) ∈ V )
39 hashxrcl ⊢ ( ( 𝐽 “ ( ℕ0 × ℕ0 ) ) ∈ V → ( ♯ ‘ ( 𝐽 “ ( ℕ0 × ℕ0 ) ) ) ∈ ℝ* )
40 38 39 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐽 “ ( ℕ0 × ℕ0 ) ) ) ∈ ℝ* )
41 fvexd ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ∈ V )
42 cnvexg ⊢ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ∈ V → ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ∈ V )
43 41 42 syl ⊢ ( 𝜑 → ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ∈ V )
44 43 imaexd ⊢ ( 𝜑 → ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) ∈ V )
45 hashxrcl ⊢ ( ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) ∈ V → ( ♯ ‘ ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) ) ∈ ℝ* )
46 44 45 syl ⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) ) ∈ ℝ* )
47 18 a1i ⊢ ( 𝜑 → 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
48 47 25 eqbrtrd ⊢ ( 𝜑 → 𝐷 ≤ ( ♯ ‘ ( 𝐽 “ ( ℕ0 × ℕ0 ) ) ) )
49 44 elexd ⊢ ( 𝜑 → ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) ∈ V )
50 nfv ⊢ Ⅎ 𝑤 𝜑
51 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ∈ V )
52 51 24 fmptd ⊢ ( 𝜑 → 𝐽 : ( ℕ0 × ℕ0 ) ⟶ V )
53 ffun ⊢ ( 𝐽 : ( ℕ0 × ℕ0 ) ⟶ V → Fun 𝐽 )
54 52 53 syl ⊢ ( 𝜑 → Fun 𝐽 )
55 24 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝐽 = ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
56 simpr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑗 = 𝑤 ) → 𝑗 = 𝑤 )
57 56 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑗 = 𝑤 ) → ( 𝐸 ‘ 𝑗 ) = ( 𝐸 ‘ 𝑤 ) )
58 57 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑗 = 𝑤 ) → ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
59 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝑤 ∈ ( ℕ0 × ℕ0 ) )
60 ovexd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ∈ V )
61 55 58 59 60 fvmptd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐽 ‘ 𝑤 ) = ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
62 eqid ⊢ ( eval1 ‘ 𝐾 ) = ( eval1 ‘ 𝐾 )
63 eqid ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ 𝐾 )
64 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
65 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
66 3 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝐾 ∈ CRing )
68 eqid ⊢ ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
69 68 64 mgpbas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
70 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝐾 ) ) = ( .g ‘ ( mulGrp ‘ 𝐾 ) )
71 66 crngringd ⊢ ( 𝜑 → 𝐾 ∈ Ring )
72 68 ringmgp ⊢ ( 𝐾 ∈ Ring → ( mulGrp ‘ 𝐾 ) ∈ Mnd )
73 71 72 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝐾 ) ∈ Mnd )
74 73 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( mulGrp ‘ 𝐾 ) ∈ Mnd )
75 6 4 7 12 aks6d1c2p1 ⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ )
76 75 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐸 ‘ 𝑤 ) ∈ ℕ )
77 76 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐸 ‘ 𝑤 ) ∈ ℕ0 )
78 68 crngmgp ⊢ ( 𝐾 ∈ CRing → ( mulGrp ‘ 𝐾 ) ∈ CMnd )
79 66 78 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝐾 ) ∈ CMnd )
80 5 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
81 79 80 70 isprimroot ⊢ ( 𝜑 → ( 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ↔ ( 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ∀ 𝑜 ∈ ℕ0 ( ( 𝑜 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) → 𝑅 ∥ 𝑜 ) ) ) )
82 16 81 mpbid ⊢ ( 𝜑 → ( 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ∀ 𝑜 ∈ ℕ0 ( ( 𝑜 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) → 𝑅 ∥ 𝑜 ) ) )
83 82 simp1d ⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
84 83 69 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ 𝐾 ) )
85 84 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝑀 ∈ ( Base ‘ 𝐾 ) )
86 69 70 74 77 85 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ∈ ( Base ‘ 𝐾 ) )
87 eqid ⊢ ( var1 ‘ 𝐾 ) = ( var1 ‘ 𝐾 )
88 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
89 3 4 2 11 9 87 88 10 aks6d1c5lem0 ⊢ ( 𝜑 → 𝐺 : ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
90 19 eleq2i ⊢ ( 𝑈 ∈ 𝑆 ↔ 𝑈 ∈ { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) } )
91 20 90 sylib ⊢ ( 𝜑 → 𝑈 ∈ { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) } )
92 elrabi ⊢ ( 𝑈 ∈ { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) } → 𝑈 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
93 92 a1i ⊢ ( 𝜑 → ( 𝑈 ∈ { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) } → 𝑈 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) )
94 91 93 mpd ⊢ ( 𝜑 → 𝑈 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
95 89 94 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑈 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
96 95 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐺 ‘ 𝑈 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
97 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
98 96 97 jca ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐺 ‘ 𝑈 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ) )
99 19 eleq2i ⊢ ( 𝑉 ∈ 𝑆 ↔ 𝑉 ∈ { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) } )
100 21 99 sylib ⊢ ( 𝜑 → 𝑉 ∈ { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) } )
101 elrabi ⊢ ( 𝑉 ∈ { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) } → 𝑉 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
102 101 a1i ⊢ ( 𝜑 → ( 𝑉 ∈ { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) } → 𝑉 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) )
103 100 102 mpd ⊢ ( 𝜑 → 𝑉 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
104 89 103 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑉 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
105 104 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐺 ‘ 𝑉 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
106 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
107 105 106 jca ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐺 ‘ 𝑉 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ) )
108 eqid ⊢ ( -g ‘ ( Poly1 ‘ 𝐾 ) ) = ( -g ‘ ( Poly1 ‘ 𝐾 ) )
109 eqid ⊢ ( -g ‘ 𝐾 ) = ( -g ‘ 𝐾 )
110 62 63 64 65 67 86 98 107 108 109 evl1subd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ( -g ‘ 𝐾 ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ) ) )
111 110 simprd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ( -g ‘ 𝐾 ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ) )
112 fveq2 ⊢ ( 𝑦 = 𝑀 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑦 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑀 ) )
113 112 oveq2d ⊢ ( 𝑦 = 𝑀 → ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑦 ) ) = ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑀 ) ) )
114 oveq2 ⊢ ( 𝑦 = 𝑀 → ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) = ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
115 114 fveq2d ⊢ ( 𝑦 = 𝑀 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
116 113 115 eqeq12d ⊢ ( 𝑦 = 𝑀 → ( ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ↔ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ) )
117 vex ⊢ 𝑘 ∈ V
118 vex ⊢ 𝑙 ∈ V
119 117 118 op1std ⊢ ( 𝑠 = ⟨ 𝑘 , 𝑙 ⟩ → ( 1st ‘ 𝑠 ) = 𝑘 )
120 119 oveq2d ⊢ ( 𝑠 = ⟨ 𝑘 , 𝑙 ⟩ → ( 𝑃 ↑ ( 1st ‘ 𝑠 ) ) = ( 𝑃 ↑ 𝑘 ) )
121 117 118 op2ndd ⊢ ( 𝑠 = ⟨ 𝑘 , 𝑙 ⟩ → ( 2nd ‘ 𝑠 ) = 𝑙 )
122 121 oveq2d ⊢ ( 𝑠 = ⟨ 𝑘 , 𝑙 ⟩ → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑠 ) ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) )
123 120 122 oveq12d ⊢ ( 𝑠 = ⟨ 𝑘 , 𝑙 ⟩ → ( ( 𝑃 ↑ ( 1st ‘ 𝑠 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑠 ) ) ) = ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
124 123 mpompt ⊢ ( 𝑠 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑠 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑠 ) ) ) ) = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
125 12 eqcomi ⊢ ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) = 𝐸
126 124 125 eqtri ⊢ ( 𝑠 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑠 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑠 ) ) ) ) = 𝐸
127 126 eqcomi ⊢ 𝐸 = ( 𝑠 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑠 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑠 ) ) ) )
128 127 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝐸 = ( 𝑠 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑠 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑠 ) ) ) ) )
129 simpr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑠 = 𝑤 ) → 𝑠 = 𝑤 )
130 129 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑠 = 𝑤 ) → ( 1st ‘ 𝑠 ) = ( 1st ‘ 𝑤 ) )
131 130 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑠 = 𝑤 ) → ( 𝑃 ↑ ( 1st ‘ 𝑠 ) ) = ( 𝑃 ↑ ( 1st ‘ 𝑤 ) ) )
132 129 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑠 = 𝑤 ) → ( 2nd ‘ 𝑠 ) = ( 2nd ‘ 𝑤 ) )
133 132 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑠 = 𝑤 ) → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑠 ) ) = ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑤 ) ) )
134 131 133 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑠 = 𝑤 ) → ( ( 𝑃 ↑ ( 1st ‘ 𝑠 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑠 ) ) ) = ( ( 𝑃 ↑ ( 1st ‘ 𝑤 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑤 ) ) ) )
135 ovexd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑃 ↑ ( 1st ‘ 𝑤 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑤 ) ) ) ∈ V )
136 128 134 59 135 fvmptd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐸 ‘ 𝑤 ) = ( ( 𝑃 ↑ ( 1st ‘ 𝑤 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑤 ) ) ) )
137 3 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝐾 ∈ Field )
138 4 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝑃 ∈ ℙ )
139 5 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝑅 ∈ ℕ )
140 6 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝑁 ∈ ℕ )
141 7 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝑃 ∥ 𝑁 )
142 8 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑁 gcd 𝑅 ) = 1 )
143 ovexd ⊢ ( 𝜑 → ( 0 ... 𝐴 ) ∈ V )
144 34 143 elmapd ⊢ ( 𝜑 → ( 𝑈 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑈 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
145 94 144 mpbid ⊢ ( 𝜑 → 𝑈 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
146 145 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝑈 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
147 11 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝐴 ∈ ℕ0 )
148 xp1st ⊢ ( 𝑤 ∈ ( ℕ0 × ℕ0 ) → ( 1st ‘ 𝑤 ) ∈ ℕ0 )
149 148 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( 1st ‘ 𝑤 ) ∈ ℕ0 )
150 xp2nd ⊢ ( 𝑤 ∈ ( ℕ0 × ℕ0 ) → ( 2nd ‘ 𝑤 ) ∈ ℕ0 )
151 150 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( 2nd ‘ 𝑤 ) ∈ ℕ0 )
152 eqid ⊢ ( ( 𝑃 ↑ ( 1st ‘ 𝑤 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑤 ) ) ) = ( ( 𝑃 ↑ ( 1st ‘ 𝑤 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑤 ) ) )
153 14 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
154 15 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
155 1 2 137 138 139 140 141 142 146 10 147 149 151 152 153 154 aks6d1c1rh ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑃 ↑ ( 1st ‘ 𝑤 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑤 ) ) ) ∼ ( 𝐺 ‘ 𝑈 ) )
156 136 155 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐸 ‘ 𝑤 ) ∼ ( 𝐺 ‘ 𝑈 ) )
157 1 96 76 aks6d1c1p1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑤 ) ∼ ( 𝐺 ‘ 𝑈 ) ↔ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) )
158 156 157 mpbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) )
159 16 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
160 116 158 159 rspcdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
161 160 eqcomd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑀 ) ) )
162 17 a1i ⊢ ( 𝜑 → 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) ) )
163 162 reseq1d ⊢ ( 𝜑 → ( 𝐻 ↾ 𝑆 ) = ( ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) ) ↾ 𝑆 ) )
164 19 a1i ⊢ ( 𝜑 → 𝑆 = { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) } )
165 ssrab2 ⊢ { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) } ⊆ ( ℕ0 ↑m ( 0 ... 𝐴 ) )
166 165 a1i ⊢ ( 𝜑 → { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) } ⊆ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
167 164 166 eqsstrd ⊢ ( 𝜑 → 𝑆 ⊆ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
168 167 resmptd ⊢ ( 𝜑 → ( ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) ) ↾ 𝑆 ) = ( ℎ ∈ 𝑆 ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) ) )
169 163 168 eqtrd ⊢ ( 𝜑 → ( 𝐻 ↾ 𝑆 ) = ( ℎ ∈ 𝑆 ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) ) )
170 simpr ⊢ ( ( 𝜑 ∧ ℎ = 𝑈 ) → ℎ = 𝑈 )
171 170 fveq2d ⊢ ( ( 𝜑 ∧ ℎ = 𝑈 ) → ( 𝐺 ‘ ℎ ) = ( 𝐺 ‘ 𝑈 ) )
172 171 fveq2d ⊢ ( ( 𝜑 ∧ ℎ = 𝑈 ) → ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) = ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) )
173 172 fveq1d ⊢ ( ( 𝜑 ∧ ℎ = 𝑈 ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑀 ) )
174 fvexd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑀 ) ∈ V )
175 169 173 20 174 fvmptd ⊢ ( 𝜑 → ( ( 𝐻 ↾ 𝑆 ) ‘ 𝑈 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑀 ) )
176 175 eqcomd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑀 ) = ( ( 𝐻 ↾ 𝑆 ) ‘ 𝑈 ) )
177 simpr ⊢ ( ( 𝜑 ∧ ℎ = 𝑉 ) → ℎ = 𝑉 )
178 177 fveq2d ⊢ ( ( 𝜑 ∧ ℎ = 𝑉 ) → ( 𝐺 ‘ ℎ ) = ( 𝐺 ‘ 𝑉 ) )
179 178 fveq2d ⊢ ( ( 𝜑 ∧ ℎ = 𝑉 ) → ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) = ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) )
180 179 fveq1d ⊢ ( ( 𝜑 ∧ ℎ = 𝑉 ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑀 ) )
181 fvexd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑀 ) ∈ V )
182 169 180 21 181 fvmptd ⊢ ( 𝜑 → ( ( 𝐻 ↾ 𝑆 ) ‘ 𝑉 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑀 ) )
183 176 22 182 3eqtrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑀 ) )
184 183 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑀 ) )
185 184 oveq2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ 𝑀 ) ) = ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑀 ) ) )
186 161 185 eqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑀 ) ) )
187 fveq2 ⊢ ( 𝑦 = 𝑀 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑦 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑀 ) )
188 187 oveq2d ⊢ ( 𝑦 = 𝑀 → ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑦 ) ) = ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑀 ) ) )
189 114 fveq2d ⊢ ( 𝑦 = 𝑀 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
190 188 189 eqeq12d ⊢ ( 𝑦 = 𝑀 → ( ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ↔ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ) )
191 34 143 elmapd ⊢ ( 𝜑 → ( 𝑉 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑉 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
192 103 191 mpbid ⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
193 192 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝑉 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
194 1 2 137 138 139 140 141 142 193 10 147 149 151 152 153 154 aks6d1c1rh ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑃 ↑ ( 1st ‘ 𝑤 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑤 ) ) ) ∼ ( 𝐺 ‘ 𝑉 ) )
195 136 194 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐸 ‘ 𝑤 ) ∼ ( 𝐺 ‘ 𝑉 ) )
196 1 105 76 aks6d1c1p1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑤 ) ∼ ( 𝐺 ‘ 𝑉 ) ↔ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) )
197 195 196 mpbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) )
198 190 197 159 rspcdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
199 186 198 eqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
200 66 crnggrpd ⊢ ( 𝜑 → 𝐾 ∈ Grp )
201 200 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → 𝐾 ∈ Grp )
202 62 63 64 65 67 86 96 fveval1fvcl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ∈ ( Base ‘ 𝐾 ) )
203 62 63 64 65 67 86 105 fveval1fvcl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ∈ ( Base ‘ 𝐾 ) )
204 eqid ⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
205 64 204 109 grpsubeq0 ⊢ ( ( 𝐾 ∈ Grp ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ( -g ‘ 𝐾 ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ) = ( 0g ‘ 𝐾 ) ↔ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ) )
206 201 202 203 205 syl3anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ( -g ‘ 𝐾 ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ) = ( 0g ‘ 𝐾 ) ↔ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ) )
207 199 206 mpbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ( -g ‘ 𝐾 ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑉 ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ) = ( 0g ‘ 𝐾 ) )
208 111 207 eqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( 0g ‘ 𝐾 ) )
209 fvexd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ∈ V )
210 elsng ⊢ ( ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ∈ V → ( ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ∈ { ( 0g ‘ 𝐾 ) } ↔ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( 0g ‘ 𝐾 ) ) )
211 209 210 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ∈ { ( 0g ‘ 𝐾 ) } ↔ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( 0g ‘ 𝐾 ) ) )
212 208 211 mpbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ∈ { ( 0g ‘ 𝐾 ) } )
213 eqid ⊢ ( 𝐾 ↑s ( Base ‘ 𝐾 ) ) = ( 𝐾 ↑s ( Base ‘ 𝐾 ) )
214 62 63 213 64 evl1rhm ⊢ ( 𝐾 ∈ CRing → ( eval1 ‘ 𝐾 ) ∈ ( ( Poly1 ‘ 𝐾 ) RingHom ( 𝐾 ↑s ( Base ‘ 𝐾 ) ) ) )
215 66 214 syl ⊢ ( 𝜑 → ( eval1 ‘ 𝐾 ) ∈ ( ( Poly1 ‘ 𝐾 ) RingHom ( 𝐾 ↑s ( Base ‘ 𝐾 ) ) ) )
216 eqid ⊢ ( Base ‘ ( 𝐾 ↑s ( Base ‘ 𝐾 ) ) ) = ( Base ‘ ( 𝐾 ↑s ( Base ‘ 𝐾 ) ) )
217 65 216 rhmf ⊢ ( ( eval1 ‘ 𝐾 ) ∈ ( ( Poly1 ‘ 𝐾 ) RingHom ( 𝐾 ↑s ( Base ‘ 𝐾 ) ) ) → ( eval1 ‘ 𝐾 ) : ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ⟶ ( Base ‘ ( 𝐾 ↑s ( Base ‘ 𝐾 ) ) ) )
218 215 217 syl ⊢ ( 𝜑 → ( eval1 ‘ 𝐾 ) : ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ⟶ ( Base ‘ ( 𝐾 ↑s ( Base ‘ 𝐾 ) ) ) )
219 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) ∈ V )
220 213 64 pwsbas ⊢ ( ( 𝐾 ∈ Field ∧ ( Base ‘ 𝐾 ) ∈ V ) → ( ( Base ‘ 𝐾 ) ↑m ( Base ‘ 𝐾 ) ) = ( Base ‘ ( 𝐾 ↑s ( Base ‘ 𝐾 ) ) ) )
221 3 219 220 syl2anc ⊢ ( 𝜑 → ( ( Base ‘ 𝐾 ) ↑m ( Base ‘ 𝐾 ) ) = ( Base ‘ ( 𝐾 ↑s ( Base ‘ 𝐾 ) ) ) )
222 221 feq3d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) : ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ⟶ ( ( Base ‘ 𝐾 ) ↑m ( Base ‘ 𝐾 ) ) ↔ ( eval1 ‘ 𝐾 ) : ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ⟶ ( Base ‘ ( 𝐾 ↑s ( Base ‘ 𝐾 ) ) ) ) )
223 218 222 mpbird ⊢ ( 𝜑 → ( eval1 ‘ 𝐾 ) : ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ⟶ ( ( Base ‘ 𝐾 ) ↑m ( Base ‘ 𝐾 ) ) )
224 63 ply1ring ⊢ ( 𝐾 ∈ Ring → ( Poly1 ‘ 𝐾 ) ∈ Ring )
225 71 224 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Ring )
226 ringgrp ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ Ring → ( Poly1 ‘ 𝐾 ) ∈ Grp )
227 225 226 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Grp )
228 65 108 grpsubcl ⊢ ( ( ( Poly1 ‘ 𝐾 ) ∈ Grp ∧ ( 𝐺 ‘ 𝑈 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( 𝐺 ‘ 𝑉 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) → ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
229 227 95 104 228 syl3anc ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
230 223 229 ffvelcdmd ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ∈ ( ( Base ‘ 𝐾 ) ↑m ( Base ‘ 𝐾 ) ) )
231 219 219 elmapd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ∈ ( ( Base ‘ 𝐾 ) ↑m ( Base ‘ 𝐾 ) ) ↔ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) ) )
232 230 231 mpbid ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) )
233 232 ffund ⊢ ( 𝜑 → Fun ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) )
234 233 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → Fun ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) )
235 232 ffnd ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) Fn ( Base ‘ 𝐾 ) )
236 235 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) Fn ( Base ‘ 𝐾 ) )
237 236 fndmd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → dom ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) = ( Base ‘ 𝐾 ) )
238 237 eqcomd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( Base ‘ 𝐾 ) = dom ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) )
239 86 238 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ∈ dom ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) )
240 fvimacnv ⊢ ( ( Fun ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ∧ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ∈ dom ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ) → ( ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ∈ { ( 0g ‘ 𝐾 ) } ↔ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ∈ ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) ) )
241 234 239 240 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) ‘ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ∈ { ( 0g ‘ 𝐾 ) } ↔ ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ∈ ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) ) )
242 212 241 mpbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑤 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ∈ ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) )
243 61 242 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐽 ‘ 𝑤 ) ∈ ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) )
244 50 54 243 funimassd ⊢ ( 𝜑 → ( 𝐽 “ ( ℕ0 × ℕ0 ) ) ⊆ ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) )
245 hashss ⊢ ( ( ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) ∈ V ∧ ( 𝐽 “ ( ℕ0 × ℕ0 ) ) ⊆ ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) ) → ( ♯ ‘ ( 𝐽 “ ( ℕ0 × ℕ0 ) ) ) ≤ ( ♯ ‘ ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) ) )
246 49 244 245 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐽 “ ( ℕ0 × ℕ0 ) ) ) ≤ ( ♯ ‘ ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) ) )
247 31 40 46 48 246 xrletrd ⊢ ( 𝜑 → 𝐷 ≤ ( ♯ ‘ ( ◡ ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑈 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑉 ) ) ) “ { ( 0g ‘ 𝐾 ) } ) ) )