Metamath Proof Explorer

Theorem aks6d1c6lem1

Description: Lemma for claim 6, deduce exact degree of the polynomial. (Contributed by metakunt, 7-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 ) }
aks6d1c6lem1.1 ⊢ ( 𝜑 → 𝑈 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
Assertion aks6d1c6lem1 ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) = Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑈 ‘ 𝑡 ) )

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 aks6d1c6lem1.1 ⊢ ( 𝜑 → 𝑈 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
21 10 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) )
22 21 fveq1d ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑈 ) = ( ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ 𝑈 ) )
23 22 fveq2d ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) = ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ 𝑈 ) ) )
24 eqidd ⊢ ( 𝜑 → ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) )
25 simplr ⊢ ( ( ( 𝜑 ∧ 𝑔 = 𝑈 ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑔 = 𝑈 )
26 25 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 = 𝑈 ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑔 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) )
27 26 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 = 𝑈 ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) = ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) )
28 27 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑔 = 𝑈 ) → ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) = ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) )
29 28 oveq2d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝑈 ) → ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) = ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
30 ovexd ⊢ ( 𝜑 → ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ V )
31 24 29 20 30 fvmptd ⊢ ( 𝜑 → ( ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ 𝑈 ) = ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
32 31 fveq2d ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ 𝑈 ) ) = ( ( deg1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) )
33 fldidom ⊢ ( 𝐾 ∈ Field → 𝐾 ∈ IDomn )
34 3 33 syl ⊢ ( 𝜑 → 𝐾 ∈ IDomn )
35 fzfid ⊢ ( 𝜑 → ( 0 ... 𝐴 ) ∈ Fin )
36 eqid ⊢ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) = ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) )
37 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
38 36 37 mgpbas ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
39 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
40 3 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
41 crngring ⊢ ( 𝐾 ∈ CRing → 𝐾 ∈ Ring )
42 40 41 syl ⊢ ( 𝜑 → 𝐾 ∈ Ring )
43 eqid ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ 𝐾 )
44 43 ply1ring ⊢ ( 𝐾 ∈ Ring → ( Poly1 ‘ 𝐾 ) ∈ Ring )
45 42 44 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Ring )
46 36 ringmgp ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ Ring → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd )
47 45 46 syl ⊢ ( 𝜑 → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd )
49 nn0ex ⊢ ℕ0 ∈ V
50 49 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
51 ovexd ⊢ ( 𝜑 → ( 0 ... 𝐴 ) ∈ V )
52 50 51 elmapd ⊢ ( 𝜑 → ( 𝑈 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑈 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
53 20 52 mpbid ⊢ ( 𝜑 → 𝑈 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
54 53 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑈 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
55 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑖 ∈ ( 0 ... 𝐴 ) )
56 54 55 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑈 ‘ 𝑖 ) ∈ ℕ0 )
57 2fveq3 ⊢ ( 𝑡 = 𝑖 → ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) = ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) )
58 57 oveq2d ⊢ ( 𝑡 = 𝑖 → ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) = ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) )
59 58 eleq1d ⊢ ( 𝑡 = 𝑖 → ( ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↔ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) )
60 ringmnd ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ Ring → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
61 45 60 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
63 42 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → 𝐾 ∈ Ring )
64 eqid ⊢ ( var1 ‘ 𝐾 ) = ( var1 ‘ 𝐾 )
65 64 43 37 vr1cl ⊢ ( 𝐾 ∈ Ring → ( var1 ‘ 𝐾 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
66 63 65 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( var1 ‘ 𝐾 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
67 eqid ⊢ ( ℤRHom ‘ 𝐾 ) = ( ℤRHom ‘ 𝐾 )
68 67 zrhrhm ⊢ ( 𝐾 ∈ Ring → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) )
69 42 68 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) )
70 zringbas ⊢ ℤ = ( Base ‘ ℤring )
71 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
72 70 71 rhmf ⊢ ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
73 69 72 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
74 73 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
75 elfzelz ⊢ ( 𝑡 ∈ ( 0 ... 𝐴 ) → 𝑡 ∈ ℤ )
76 75 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → 𝑡 ∈ ℤ )
77 74 76 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ∈ ( Base ‘ 𝐾 ) )
78 eqid ⊢ ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) = ( algSc ‘ ( Poly1 ‘ 𝐾 ) )
79 43 78 71 37 ply1sclcl ⊢ ( ( 𝐾 ∈ Ring ∧ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
80 63 77 79 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
81 eqid ⊢ ( +g ‘ ( Poly1 ‘ 𝐾 ) ) = ( +g ‘ ( Poly1 ‘ 𝐾 ) )
82 37 81 mndcl ⊢ ( ( ( Poly1 ‘ 𝐾 ) ∈ Mnd ∧ ( var1 ‘ 𝐾 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) → ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
83 62 66 80 82 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
84 83 ralrimiva ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 0 ... 𝐴 ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
85 84 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ∀ 𝑡 ∈ ( 0 ... 𝐴 ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
86 59 85 55 rspcdva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
87 38 39 48 56 86 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
88 43 ply1idom ⊢ ( 𝐾 ∈ IDomn → ( Poly1 ‘ 𝐾 ) ∈ IDomn )
89 34 88 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ IDomn )
90 89 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( Poly1 ‘ 𝐾 ) ∈ IDomn )
91 58 neeq1d ⊢ ( 𝑡 = 𝑖 → ( ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ↔ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ) )
92 eqid ⊢ ( deg1 ‘ 𝐾 ) = ( deg1 ‘ 𝐾 )
93 92 43 37 deg1xrcl ⊢ ( ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ∈ ℝ* )
94 80 93 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ∈ ℝ* )
95 0xr ⊢ 0 ∈ ℝ*
96 95 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → 0 ∈ ℝ* )
97 1xr ⊢ 1 ∈ ℝ*
98 97 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → 1 ∈ ℝ* )
99 92 43 71 78 deg1sclle ⊢ ( ( 𝐾 ∈ Ring ∧ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ≤ 0 )
100 63 77 99 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ≤ 0 )
101 0lt1 ⊢ 0 < 1
102 101 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → 0 < 1 )
103 94 96 98 100 102 xrlelttrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) < 1 )
104 38 39 mulg1 ⊢ ( ( var1 ‘ 𝐾 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) → ( 1 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) = ( var1 ‘ 𝐾 ) )
105 66 104 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( 1 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) = ( var1 ‘ 𝐾 ) )
106 105 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( var1 ‘ 𝐾 ) = ( 1 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) )
107 106 fveq2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( var1 ‘ 𝐾 ) ) = ( ( deg1 ‘ 𝐾 ) ‘ ( 1 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ) )
108 isfld ⊢ ( 𝐾 ∈ Field ↔ ( 𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing ) )
109 drngnzr ⊢ ( 𝐾 ∈ DivRing → 𝐾 ∈ NzRing )
110 109 adantr ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing ) → 𝐾 ∈ NzRing )
111 108 110 sylbi ⊢ ( 𝐾 ∈ Field → 𝐾 ∈ NzRing )
112 3 111 syl ⊢ ( 𝜑 → 𝐾 ∈ NzRing )
113 112 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → 𝐾 ∈ NzRing )
114 1nn0 ⊢ 1 ∈ ℕ0
115 114 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → 1 ∈ ℕ0 )
116 92 43 64 36 39 deg1pw ⊢ ( ( 𝐾 ∈ NzRing ∧ 1 ∈ ℕ0 ) → ( ( deg1 ‘ 𝐾 ) ‘ ( 1 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ) = 1 )
117 113 115 116 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( 1 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ) = 1 )
118 107 117 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → 1 = ( ( deg1 ‘ 𝐾 ) ‘ ( var1 ‘ 𝐾 ) ) )
119 103 118 breqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) < ( ( deg1 ‘ 𝐾 ) ‘ ( var1 ‘ 𝐾 ) ) )
120 43 92 63 37 81 66 80 119 deg1add ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) = ( ( deg1 ‘ 𝐾 ) ‘ ( var1 ‘ 𝐾 ) ) )
121 107 117 eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( var1 ‘ 𝐾 ) ) = 1 )
122 120 121 eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) = 1 )
123 122 115 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) ∈ ℕ0 )
124 eqid ⊢ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) = ( 0g ‘ ( Poly1 ‘ 𝐾 ) )
125 92 43 124 37 deg1nn0clb ⊢ ( ( 𝐾 ∈ Ring ∧ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) → ( ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ↔ ( ( deg1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) ∈ ℕ0 ) )
126 63 83 125 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ↔ ( ( deg1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) ∈ ℕ0 ) )
127 123 126 mpbird ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) )
128 127 ralrimiva ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 0 ... 𝐴 ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) )
129 128 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ∀ 𝑡 ∈ ( 0 ... 𝐴 ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) )
130 91 129 55 rspcdva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) )
131 90 86 130 56 39 idomnnzpownz ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) )
132 87 131 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ) )
133 132 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ) )
134 34 35 133 deg1gprod ⊢ ( 𝜑 → ( ( ( deg1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) = Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ 𝑡 ) ) ∧ 0 ≤ ( ( deg1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) )
135 134 simpld ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) = Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ 𝑡 ) ) )
136 eqidd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) = ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) )
137 simpr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑖 = 𝑡 ) → 𝑖 = 𝑡 )
138 137 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑖 = 𝑡 ) → ( 𝑈 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑡 ) )
139 137 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑖 = 𝑡 ) → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) )
140 139 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑖 = 𝑡 ) → ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) = ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) )
141 140 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑖 = 𝑡 ) → ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) = ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) )
142 138 141 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑖 = 𝑡 ) → ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) = ( ( 𝑈 ‘ 𝑡 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) )
143 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → 𝑡 ∈ ( 0 ... 𝐴 ) )
144 ovexd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑈 ‘ 𝑡 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) ∈ V )
145 136 142 143 144 fvmptd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ 𝑡 ) = ( ( 𝑈 ‘ 𝑡 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) )
146 145 fveq2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ 𝑡 ) ) = ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑈 ‘ 𝑡 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) ) )
147 34 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → 𝐾 ∈ IDomn )
148 53 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( 𝑈 ‘ 𝑡 ) ∈ ℕ0 )
149 147 83 127 148 39 92 deg1pow ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑈 ‘ 𝑡 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) ) = ( ( 𝑈 ‘ 𝑡 ) · ( ( deg1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) ) )
150 122 oveq2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑈 ‘ 𝑡 ) · ( ( deg1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) ) = ( ( 𝑈 ‘ 𝑡 ) · 1 ) )
151 148 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( 𝑈 ‘ 𝑡 ) ∈ ℂ )
152 151 mulridd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑈 ‘ 𝑡 ) · 1 ) = ( 𝑈 ‘ 𝑡 ) )
153 150 152 eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑈 ‘ 𝑡 ) · ( ( deg1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) ) = ( 𝑈 ‘ 𝑡 ) )
154 149 153 eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑈 ‘ 𝑡 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑡 ) ) ) ) ) = ( 𝑈 ‘ 𝑡 ) )
155 146 154 eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝐴 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ 𝑡 ) ) = ( 𝑈 ‘ 𝑡 ) )
156 155 sumeq2dv ⊢ ( 𝜑 → Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ 𝑡 ) ) = Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑈 ‘ 𝑡 ) )
157 135 156 eqtrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) = Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑈 ‘ 𝑡 ) )
158 32 157 eqtrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ 𝑈 ) ) = Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑈 ‘ 𝑡 ) )
159 23 158 eqtrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ 𝑈 ) ) = Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑈 ‘ 𝑡 ) )