Metamath Proof Explorer

Theorem aks6d1c5lem2

Description: Lemma for Claim 5, contradiction of different evaluations that map to the same. (Contributed by metakunt, 5-May-2025)

Ref Expression
Hypotheses aks6d1p5.1 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1p5.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c5.3 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c5.4 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
aks6d1c5.5 ⊢ ( 𝜑 → 𝐴 < 𝑃 )
aks6d1c5.6 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
aks6d1c5.7 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
aks6d1c5.8 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
aks6d1c5p2.1 ⊢ ( 𝜑 → 𝑌 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
aks6d1c5p2.2 ⊢ ( 𝜑 → 𝑍 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
aks6d1c5p2.3 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑍 ) )
aks6d1c5p2.4 ⊢ ( 𝜑 → 𝑊 ∈ ( 0 ... 𝐴 ) )
aks6d1c5p2.5 ⊢ ( 𝜑 → ( 𝑌 ‘ 𝑊 ) < ( 𝑍 ‘ 𝑊 ) )
Assertion aks6d1c5lem2 ( 𝜑 → ( 0g ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 aks6d1p5.1 ⊢ ( 𝜑 → 𝐾 ∈ Field )
2 aks6d1p5.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
3 aks6d1c5.3 ⊢ 𝑃 = ( chr ‘ 𝐾 )
4 aks6d1c5.4 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
5 aks6d1c5.5 ⊢ ( 𝜑 → 𝐴 < 𝑃 )
6 aks6d1c5.6 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
7 aks6d1c5.7 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
8 aks6d1c5.8 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
9 aks6d1c5p2.1 ⊢ ( 𝜑 → 𝑌 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
10 aks6d1c5p2.2 ⊢ ( 𝜑 → 𝑍 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
11 aks6d1c5p2.3 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑍 ) )
12 aks6d1c5p2.4 ⊢ ( 𝜑 → 𝑊 ∈ ( 0 ... 𝐴 ) )
13 aks6d1c5p2.5 ⊢ ( 𝜑 → ( 𝑌 ‘ 𝑊 ) < ( 𝑍 ‘ 𝑊 ) )
14 eqid ⊢ ( eval1 ‘ 𝐾 ) = ( eval1 ‘ 𝐾 )
15 eqid ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ 𝐾 )
16 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
18 isfld ⊢ ( 𝐾 ∈ Field ↔ ( 𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing ) )
19 18 simprbi ⊢ ( 𝐾 ∈ Field → 𝐾 ∈ CRing )
20 1 19 syl ⊢ ( 𝜑 → 𝐾 ∈ CRing )
21 20 crngringd ⊢ ( 𝜑 → 𝐾 ∈ Ring )
22 eqid ⊢ ( ℤRHom ‘ 𝐾 ) = ( ℤRHom ‘ 𝐾 )
23 22 zrhrhm ⊢ ( 𝐾 ∈ Ring → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) )
24 21 23 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) )
25 zringbas ⊢ ℤ = ( Base ‘ ℤring )
26 25 16 rhmf ⊢ ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
27 24 26 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
28 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
29 12 elfzelzd ⊢ ( 𝜑 → 𝑊 ∈ ℤ )
30 28 29 zsubcld ⊢ ( 𝜑 → ( 0 − 𝑊 ) ∈ ℤ )
31 27 30 ffvelcdmd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
32 eqid ⊢ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) = ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) )
33 32 17 mgpbas ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
34 15 ply1crng ⊢ ( 𝐾 ∈ CRing → ( Poly1 ‘ 𝐾 ) ∈ CRing )
35 20 34 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ CRing )
36 32 crngmgp ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ CRing → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ CMnd )
37 35 36 syl ⊢ ( 𝜑 → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ CMnd )
38 37 cmnmndd ⊢ ( 𝜑 → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd )
39 nn0ex ⊢ ℕ0 ∈ V
40 39 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
41 ovexd ⊢ ( 𝜑 → ( 0 ... 𝐴 ) ∈ V )
42 elmapg ⊢ ( ( ℕ0 ∈ V ∧ ( 0 ... 𝐴 ) ∈ V ) → ( 𝑌 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑌 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
43 40 41 42 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑌 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
44 9 43 mpbid ⊢ ( 𝜑 → 𝑌 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
45 44 12 ffvelcdmd ⊢ ( 𝜑 → ( 𝑌 ‘ 𝑊 ) ∈ ℕ0 )
46 45 nn0zd ⊢ ( 𝜑 → ( 𝑌 ‘ 𝑊 ) ∈ ℤ )
47 46 46 zsubcld ⊢ ( 𝜑 → ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℤ )
48 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
49 48 leidd ⊢ ( 𝜑 → 0 ≤ 0 )
50 45 nn0red ⊢ ( 𝜑 → ( 𝑌 ‘ 𝑊 ) ∈ ℝ )
51 50 recnd ⊢ ( 𝜑 → ( 𝑌 ‘ 𝑊 ) ∈ ℂ )
52 51 subidd ⊢ ( 𝜑 → ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) = 0 )
53 52 eqcomd ⊢ ( 𝜑 → 0 = ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) )
54 49 53 breqtrd ⊢ ( 𝜑 → 0 ≤ ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) )
55 47 54 jca ⊢ ( 𝜑 → ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℤ ∧ 0 ≤ ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ) )
56 elnn0z ⊢ ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℕ0 ↔ ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℤ ∧ 0 ≤ ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ) )
57 55 56 sylibr ⊢ ( 𝜑 → ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℕ0 )
58 14 6 16 15 17 20 31 evl1vard ⊢ ( 𝜑 → ( 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑋 ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) )
59 eqid ⊢ ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) = ( algSc ‘ ( Poly1 ‘ 𝐾 ) )
60 27 29 ffvelcdmd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
61 14 15 16 59 17 20 60 31 evl1scad ⊢ ( 𝜑 → ( ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) )
62 eqid ⊢ ( +g ‘ ( Poly1 ‘ 𝐾 ) ) = ( +g ‘ ( Poly1 ‘ 𝐾 ) )
63 eqid ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
64 14 15 16 17 20 31 58 61 62 63 evl1addd ⊢ ( 𝜑 → ( ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
65 64 simpld ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
66 33 7 38 57 65 mulgnn0cld ⊢ ( 𝜑 → ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
67 52 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) = ( 0 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
68 eqid ⊢ ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
69 33 68 7 mulg0 ⊢ ( ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) → ( 0 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) = ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
70 65 69 syl ⊢ ( 𝜑 → ( 0 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) = ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
71 67 70 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) = ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
72 71 fveq2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( eval1 ‘ 𝐾 ) ‘ ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ) )
73 72 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) )
74 eqid ⊢ ( 1r ‘ ( Poly1 ‘ 𝐾 ) ) = ( 1r ‘ ( Poly1 ‘ 𝐾 ) )
75 32 74 ringidval ⊢ ( 1r ‘ ( Poly1 ‘ 𝐾 ) ) = ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
76 75 eqcomi ⊢ ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( 1r ‘ ( Poly1 ‘ 𝐾 ) )
77 76 a1i ⊢ ( 𝜑 → ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( 1r ‘ ( Poly1 ‘ 𝐾 ) ) )
78 77 fveq2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) ‘ ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ) = ( ( eval1 ‘ 𝐾 ) ‘ ( 1r ‘ ( Poly1 ‘ 𝐾 ) ) ) )
79 78 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 1r ‘ ( Poly1 ‘ 𝐾 ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) )
80 15 6 32 7 ply1idvr1 ⊢ ( 𝐾 ∈ Ring → ( 0 ↑ 𝑋 ) = ( 1r ‘ ( Poly1 ‘ 𝐾 ) ) )
81 80 eqcomd ⊢ ( 𝐾 ∈ Ring → ( 1r ‘ ( Poly1 ‘ 𝐾 ) ) = ( 0 ↑ 𝑋 ) )
82 21 81 syl ⊢ ( 𝜑 → ( 1r ‘ ( Poly1 ‘ 𝐾 ) ) = ( 0 ↑ 𝑋 ) )
83 82 fveq2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) ‘ ( 1r ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( ( eval1 ‘ 𝐾 ) ‘ ( 0 ↑ 𝑋 ) ) )
84 83 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 1r ‘ ( Poly1 ‘ 𝐾 ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 0 ↑ 𝑋 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) )
85 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝐾 ) ) = ( .g ‘ ( mulGrp ‘ 𝐾 ) )
86 53 57 eqeltrd ⊢ ( 𝜑 → 0 ∈ ℕ0 )
87 14 15 16 17 20 31 58 7 85 86 evl1expd ⊢ ( 𝜑 → ( ( 0 ↑ 𝑋 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 0 ↑ 𝑋 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 0 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) )
88 87 simprd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 0 ↑ 𝑋 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 0 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) )
89 eqid ⊢ ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
90 89 16 mgpbas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
91 90 a1i ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
92 31 91 eleqtrd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
93 eqid ⊢ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
94 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) )
95 93 94 85 mulg0 ⊢ ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) → ( 0 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) )
96 92 95 syl ⊢ ( 𝜑 → ( 0 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) )
97 eqid ⊢ ( 1r ‘ 𝐾 ) = ( 1r ‘ 𝐾 )
98 89 97 ringidval ⊢ ( 1r ‘ 𝐾 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) )
99 98 eqcomi ⊢ ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) = ( 1r ‘ 𝐾 )
100 99 a1i ⊢ ( 𝜑 → ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) = ( 1r ‘ 𝐾 ) )
101 96 100 eqtrd ⊢ ( 𝜑 → ( 0 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 1r ‘ 𝐾 ) )
102 88 101 eqtrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 0 ↑ 𝑋 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 1r ‘ 𝐾 ) )
103 84 102 eqtrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 1r ‘ ( Poly1 ‘ 𝐾 ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 1r ‘ 𝐾 ) )
104 79 103 eqtrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 1r ‘ 𝐾 ) )
105 73 104 eqtrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 1r ‘ 𝐾 ) )
106 66 105 jca ⊢ ( 𝜑 → ( ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 1r ‘ 𝐾 ) ) )
107 fzfid ⊢ ( 𝜑 → ( 0 ... 𝐴 ) ∈ Fin )
108 diffi ⊢ ( ( 0 ... 𝐴 ) ∈ Fin → ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ∈ Fin )
109 107 108 syl ⊢ ( 𝜑 → ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ∈ Fin )
110 38 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd )
111 44 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝑌 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
112 eldifi ⊢ ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) → 𝑖 ∈ ( 0 ... 𝐴 ) )
113 112 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝑖 ∈ ( 0 ... 𝐴 ) )
114 111 113 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( 𝑌 ‘ 𝑖 ) ∈ ℕ0 )
115 35 crngringd ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Ring )
116 ringcmn ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ Ring → ( Poly1 ‘ 𝐾 ) ∈ CMnd )
117 115 116 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ CMnd )
118 cmnmnd ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ CMnd → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
119 117 118 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
120 119 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
121 58 simpld ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
122 121 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
123 21 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝐾 ∈ Ring )
124 123 23 26 3syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
125 113 elfzelzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝑖 ∈ ℤ )
126 124 125 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝐾 ) )
127 15 59 16 17 ply1sclcl ⊢ ( ( 𝐾 ∈ Ring ∧ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
128 123 126 127 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
129 17 62 mndcl ⊢ ( ( ( Poly1 ‘ 𝐾 ) ∈ Mnd ∧ 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
130 120 122 128 129 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
131 33 7 110 114 130 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
132 131 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
133 33 37 109 132 gsummptcl ⊢ ( 𝜑 → ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
134 132 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
135 134 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
136 14 15 32 16 17 89 20 31 135 109 evl1gprodd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( mulGrp ‘ 𝐾 ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) )
137 133 136 jca ⊢ ( 𝜑 → ( ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( mulGrp ‘ 𝐾 ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) ) )
138 eqid ⊢ ( .r ‘ ( Poly1 ‘ 𝐾 ) ) = ( .r ‘ ( Poly1 ‘ 𝐾 ) )
139 32 138 mgpplusg ⊢ ( .r ‘ ( Poly1 ‘ 𝐾 ) ) = ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
140 139 eqcomi ⊢ ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( .r ‘ ( Poly1 ‘ 𝐾 ) )
141 eqid ⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
142 14 15 16 17 20 31 106 137 140 141 evl1muld ⊢ ( 𝜑 → ( ( ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( 1r ‘ 𝐾 ) ( .r ‘ 𝐾 ) ( ( mulGrp ‘ 𝐾 ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) ) ) )
143 142 simprd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( 1r ‘ 𝐾 ) ( .r ‘ 𝐾 ) ( ( mulGrp ‘ 𝐾 ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) ) )
144 fldidom ⊢ ( 𝐾 ∈ Field → 𝐾 ∈ IDomn )
145 1 144 syl ⊢ ( 𝜑 → 𝐾 ∈ IDomn )
146 isidom ⊢ ( 𝐾 ∈ IDomn ↔ ( 𝐾 ∈ CRing ∧ 𝐾 ∈ Domn ) )
147 145 146 sylib ⊢ ( 𝜑 → ( 𝐾 ∈ CRing ∧ 𝐾 ∈ Domn ) )
148 147 simprd ⊢ ( 𝜑 → 𝐾 ∈ Domn )
149 98 a1i ⊢ ( 𝜑 → ( 1r ‘ 𝐾 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) )
150 89 ringmgp ⊢ ( 𝐾 ∈ Ring → ( mulGrp ‘ 𝐾 ) ∈ Mnd )
151 21 150 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝐾 ) ∈ Mnd )
152 90 94 mndidcl ⊢ ( ( mulGrp ‘ 𝐾 ) ∈ Mnd → ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ∈ ( Base ‘ 𝐾 ) )
153 151 152 syl ⊢ ( 𝜑 → ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ∈ ( Base ‘ 𝐾 ) )
154 149 153 eqeltrd ⊢ ( 𝜑 → ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
155 1 flddrngd ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
156 eqid ⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
157 156 97 drngunz ⊢ ( 𝐾 ∈ DivRing → ( 1r ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) )
158 155 157 syl ⊢ ( 𝜑 → ( 1r ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) )
159 154 158 jca ⊢ ( 𝜑 → ( ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 1r ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) ) )
160 89 crngmgp ⊢ ( 𝐾 ∈ CRing → ( mulGrp ‘ 𝐾 ) ∈ CMnd )
161 20 160 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝐾 ) ∈ CMnd )
162 20 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝐾 ∈ CRing )
163 31 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
164 14 15 16 17 162 163 131 fveval1fvcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ∈ ( Base ‘ 𝐾 ) )
165 164 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ∈ ( Base ‘ 𝐾 ) )
166 90 161 109 165 gsummptcl ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝐾 ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) ∈ ( Base ‘ 𝐾 ) )
167 33 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
168 130 167 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
169 33 eqcomi ⊢ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
170 169 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
171 168 170 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
172 eqidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) )
173 171 172 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) )
174 14 15 16 17 162 163 173 7 85 114 evl1expd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( 𝑌 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) )
175 174 simprd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( 𝑌 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) )
176 145 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝐾 ∈ IDomn )
177 14 15 16 17 162 163 171 fveval1fvcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ∈ ( Base ‘ 𝐾 ) )
178 eldifsni ⊢ ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) → 𝑖 ≠ 𝑊 )
179 178 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝑖 ≠ 𝑊 )
180 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝐾 ∈ Field )
181 2 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝑃 ∈ ℙ )
182 4 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝐴 ∈ ℕ0 )
183 5 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝐴 < 𝑃 )
184 12 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝑊 ∈ ( 0 ... 𝐴 ) )
185 180 181 3 182 183 6 7 8 113 184 aks6d1c5lem1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( 𝑖 = 𝑊 ↔ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 0g ‘ 𝐾 ) ) )
186 185 necon3bid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( 𝑖 ≠ 𝑊 ↔ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ≠ ( 0g ‘ 𝐾 ) ) )
187 179 186 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ≠ ( 0g ‘ 𝐾 ) )
188 176 177 187 114 85 idomnnzpownz ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( 𝑌 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ≠ ( 0g ‘ 𝐾 ) )
189 175 188 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ≠ ( 0g ‘ 𝐾 ) )
190 89 145 109 164 189 idomnnzgmulnz ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝐾 ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) ≠ ( 0g ‘ 𝐾 ) )
191 166 190 jca ⊢ ( 𝜑 → ( ( ( mulGrp ‘ 𝐾 ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( mulGrp ‘ 𝐾 ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) ≠ ( 0g ‘ 𝐾 ) ) )
192 16 141 156 domnmuln0 ⊢ ( ( 𝐾 ∈ Domn ∧ ( ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 1r ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) ) ∧ ( ( ( mulGrp ‘ 𝐾 ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( mulGrp ‘ 𝐾 ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 1r ‘ 𝐾 ) ( .r ‘ 𝐾 ) ( ( mulGrp ‘ 𝐾 ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) ) ≠ ( 0g ‘ 𝐾 ) )
193 148 159 191 192 syl3anc ⊢ ( 𝜑 → ( ( 1r ‘ 𝐾 ) ( .r ‘ 𝐾 ) ( ( mulGrp ‘ 𝐾 ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) ) ≠ ( 0g ‘ 𝐾 ) )
194 143 193 eqnetrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ≠ ( 0g ‘ 𝐾 ) )
195 194 necomd ⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) ≠ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) )
196 50 leidd ⊢ ( 𝜑 → ( 𝑌 ‘ 𝑊 ) ≤ ( 𝑌 ‘ 𝑊 ) )
197 eqid ⊢ ( quot1p ‘ 𝐾 ) = ( quot1p ‘ 𝐾 )
198 1 2 3 4 5 6 7 8 9 12 45 196 197 59 32 aks6d1c5lem3 ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) ( quot1p ‘ 𝐾 ) ( ( 𝑌 ‘ 𝑊 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) )
199 198 eqcomd ⊢ ( 𝜑 → ( ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝐺 ‘ 𝑌 ) ( quot1p ‘ 𝐾 ) ( ( 𝑌 ‘ 𝑊 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
200 11 oveq1d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) ( quot1p ‘ 𝐾 ) ( ( 𝑌 ‘ 𝑊 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( 𝐺 ‘ 𝑍 ) ( quot1p ‘ 𝐾 ) ( ( 𝑌 ‘ 𝑊 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
201 elmapg ⊢ ( ( ℕ0 ∈ V ∧ ( 0 ... 𝐴 ) ∈ V ) → ( 𝑍 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑍 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
202 40 41 201 syl2anc ⊢ ( 𝜑 → ( 𝑍 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑍 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
203 10 202 mpbid ⊢ ( 𝜑 → 𝑍 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
204 203 12 ffvelcdmd ⊢ ( 𝜑 → ( 𝑍 ‘ 𝑊 ) ∈ ℕ0 )
205 204 nn0red ⊢ ( 𝜑 → ( 𝑍 ‘ 𝑊 ) ∈ ℝ )
206 50 205 13 ltled ⊢ ( 𝜑 → ( 𝑌 ‘ 𝑊 ) ≤ ( 𝑍 ‘ 𝑊 ) )
207 1 2 3 4 5 6 7 8 10 12 45 206 197 59 32 aks6d1c5lem3 ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑍 ) ( quot1p ‘ 𝐾 ) ( ( 𝑌 ‘ 𝑊 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) )
208 199 200 207 3eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) = ( ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) )
209 208 fveq2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) = ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) )
210 209 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) )
211 204 nn0zd ⊢ ( 𝜑 → ( 𝑍 ‘ 𝑊 ) ∈ ℤ )
212 211 46 zsubcld ⊢ ( 𝜑 → ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℤ )
213 205 50 resubcld ⊢ ( 𝜑 → ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℝ )
214 50 205 posdifd ⊢ ( 𝜑 → ( ( 𝑌 ‘ 𝑊 ) < ( 𝑍 ‘ 𝑊 ) ↔ 0 < ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ) )
215 13 214 mpbid ⊢ ( 𝜑 → 0 < ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) )
216 48 213 215 ltled ⊢ ( 𝜑 → 0 ≤ ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) )
217 212 216 jca ⊢ ( 𝜑 → ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℤ ∧ 0 ≤ ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ) )
218 elnn0z ⊢ ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℕ0 ↔ ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℤ ∧ 0 ≤ ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ) )
219 217 218 sylibr ⊢ ( 𝜑 → ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℕ0 )
220 14 15 16 17 20 31 64 7 85 219 evl1expd ⊢ ( 𝜑 → ( ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
221 220 simpld ⊢ ( 𝜑 → ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
222 220 simprd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
223 rhmghm ⊢ ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring GrpHom 𝐾 ) )
224 24 223 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring GrpHom 𝐾 ) )
225 30 25 eleqtrdi ⊢ ( 𝜑 → ( 0 − 𝑊 ) ∈ ( Base ‘ ℤring ) )
226 29 25 eleqtrdi ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ ℤring ) )
227 eqid ⊢ ( Base ‘ ℤring ) = ( Base ‘ ℤring )
228 eqid ⊢ ( +g ‘ ℤring ) = ( +g ‘ ℤring )
229 227 228 63 ghmlin ⊢ ( ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring GrpHom 𝐾 ) ∧ ( 0 − 𝑊 ) ∈ ( Base ‘ ℤring ) ∧ 𝑊 ∈ ( Base ‘ ℤring ) ) → ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝑊 ) ( +g ‘ ℤring ) 𝑊 ) ) = ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) )
230 224 225 226 229 syl3anc ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝑊 ) ( +g ‘ ℤring ) 𝑊 ) ) = ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) )
231 zringplusg ⊢ + = ( +g ‘ ℤring )
232 231 eqcomi ⊢ ( +g ‘ ℤring ) = +
233 232 a1i ⊢ ( 𝜑 → ( +g ‘ ℤring ) = + )
234 233 oveqd ⊢ ( 𝜑 → ( ( 0 − 𝑊 ) ( +g ‘ ℤring ) 𝑊 ) = ( ( 0 − 𝑊 ) + 𝑊 ) )
235 234 fveq2d ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝑊 ) ( +g ‘ ℤring ) 𝑊 ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝑊 ) + 𝑊 ) ) )
236 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
237 29 zcnd ⊢ ( 𝜑 → 𝑊 ∈ ℂ )
238 236 237 npcand ⊢ ( 𝜑 → ( ( 0 − 𝑊 ) + 𝑊 ) = 0 )
239 238 fveq2d ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝑊 ) + 𝑊 ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 0 ) )
240 235 239 eqtrd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝑊 ) ( +g ‘ ℤring ) 𝑊 ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 0 ) )
241 22 156 zrh0 ⊢ ( 𝐾 ∈ Ring → ( ( ℤRHom ‘ 𝐾 ) ‘ 0 ) = ( 0g ‘ 𝐾 ) )
242 21 241 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ 0 ) = ( 0g ‘ 𝐾 ) )
243 240 242 eqtrd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝑊 ) ( +g ‘ ℤring ) 𝑊 ) ) = ( 0g ‘ 𝐾 ) )
244 230 243 eqtr3d ⊢ ( 𝜑 → ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ 𝐾 ) )
245 244 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( 0g ‘ 𝐾 ) ) )
246 219 nn0zd ⊢ ( 𝜑 → ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℤ )
247 246 215 jca ⊢ ( 𝜑 → ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℤ ∧ 0 < ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ) )
248 elnnz ⊢ ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℕ ↔ ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℤ ∧ 0 < ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ) )
249 247 248 sylibr ⊢ ( 𝜑 → ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ∈ ℕ )
250 21 249 85 ringexp0nn ⊢ ( 𝜑 → ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( 0g ‘ 𝐾 ) ) = ( 0g ‘ 𝐾 ) )
251 245 250 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( 0g ‘ 𝐾 ) )
252 222 251 eqtrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 0g ‘ 𝐾 ) )
253 221 252 jca ⊢ ( 𝜑 → ( ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 0g ‘ 𝐾 ) ) )
254 eqid ⊢ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
255 203 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝑍 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
256 255 113 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℕ0 )
257 254 7 110 256 168 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
258 257 170 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
259 258 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
260 33 37 109 259 gsummptcl ⊢ ( 𝜑 → ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
261 eqidd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) )
262 260 261 jca ⊢ ( 𝜑 → ( ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) )
263 14 15 16 17 20 31 253 262 140 141 evl1muld ⊢ ( 𝜑 → ( ( ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( 0g ‘ 𝐾 ) ( .r ‘ 𝐾 ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) ) )
264 263 simprd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( ( 0g ‘ 𝐾 ) ( .r ‘ 𝐾 ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) )
265 14 15 16 17 20 31 260 fveval1fvcl ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ∈ ( Base ‘ 𝐾 ) )
266 16 141 156 21 265 ringlzd ⊢ ( 𝜑 → ( ( 0g ‘ 𝐾 ) ( .r ‘ 𝐾 ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) ) = ( 0g ‘ 𝐾 ) )
267 264 266 eqtrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( ( 𝑍 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑍 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 0g ‘ 𝐾 ) )
268 210 267 eqtrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ( ( 𝑌 ‘ 𝑊 ) − ( 𝑌 ‘ 𝑊 ) ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝑊 ) ) ) = ( 0g ‘ 𝐾 ) )
269 195 268 neeqtrd ⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) )