Metamath Proof Explorer

Theorem aks6d1c5lem3

Description: Lemma for Claim 5, polynomial division with a linear power. (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 ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
aks6d1c5p3.1 ⊢ ( 𝜑 → 𝑌 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
aks6d1c5p3.2 ⊢ ( 𝜑 → 𝑊 ∈ ( 0 ... 𝐴 ) )
aks6d1c5p3.3 ⊢ ( 𝜑 → 𝐶 ∈ ℕ0 )
aks6d1c5p3.4 ⊢ ( 𝜑 → 𝐶 ≤ ( 𝑌 ‘ 𝑊 ) )
aks6d1c5p3.5 ⊢ 𝑄 = ( quot1p ‘ 𝐾 )
aks6d1c5p3.6 ⊢ 𝑆 = ( algSc ‘ ( Poly1 ‘ 𝐾 ) )
aks6d1c5p3.7 ⊢ 𝑀 = ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) )
Assertion aks6d1c5lem3 ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) 𝑄 ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) )

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 aks6d1c5p3.1 ⊢ ( 𝜑 → 𝑌 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
10 aks6d1c5p3.2 ⊢ ( 𝜑 → 𝑊 ∈ ( 0 ... 𝐴 ) )
11 aks6d1c5p3.3 ⊢ ( 𝜑 → 𝐶 ∈ ℕ0 )
12 aks6d1c5p3.4 ⊢ ( 𝜑 → 𝐶 ≤ ( 𝑌 ‘ 𝑊 ) )
13 aks6d1c5p3.5 ⊢ 𝑄 = ( quot1p ‘ 𝐾 )
14 aks6d1c5p3.6 ⊢ 𝑆 = ( algSc ‘ ( Poly1 ‘ 𝐾 ) )
15 aks6d1c5p3.7 ⊢ 𝑀 = ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) )
16 1 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
17 eqid ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ 𝐾 )
18 17 ply1crng ⊢ ( 𝐾 ∈ CRing → ( Poly1 ‘ 𝐾 ) ∈ CRing )
19 16 18 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ CRing )
20 crngring ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ CRing → ( Poly1 ‘ 𝐾 ) ∈ Ring )
21 19 20 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Ring )
22 eqid ⊢ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) = ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) )
23 22 ringmgp ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ Ring → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd )
24 21 23 syl ⊢ ( 𝜑 → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd )
25 15 24 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
26 15 fveq2i ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
27 nn0ex ⊢ ℕ0 ∈ V
28 27 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
29 ovexd ⊢ ( 𝜑 → ( 0 ... 𝐴 ) ∈ V )
30 elmapg ⊢ ( ( ℕ0 ∈ V ∧ ( 0 ... 𝐴 ) ∈ V ) → ( 𝑌 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑌 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
31 28 29 30 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑌 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
32 9 31 mpbid ⊢ ( 𝜑 → 𝑌 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
33 32 10 ffvelcdmd ⊢ ( 𝜑 → ( 𝑌 ‘ 𝑊 ) ∈ ℕ0 )
34 33 nn0zd ⊢ ( 𝜑 → ( 𝑌 ‘ 𝑊 ) ∈ ℤ )
35 11 nn0zd ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
36 34 35 zsubcld ⊢ ( 𝜑 → ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ∈ ℤ )
37 33 nn0red ⊢ ( 𝜑 → ( 𝑌 ‘ 𝑊 ) ∈ ℝ )
38 11 nn0red ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
39 37 38 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↔ 𝐶 ≤ ( 𝑌 ‘ 𝑊 ) ) )
40 12 39 mpbird ⊢ ( 𝜑 → 0 ≤ ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) )
41 36 40 jca ⊢ ( 𝜑 → ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ) )
42 elnn0z ⊢ ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ∈ ℕ0 ↔ ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ) )
43 41 42 sylibr ⊢ ( 𝜑 → ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ∈ ℕ0 )
44 21 ringcmnd ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ CMnd )
45 cmnmnd ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ CMnd → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
46 44 45 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
47 crngring ⊢ ( 𝐾 ∈ CRing → 𝐾 ∈ Ring )
48 16 47 syl ⊢ ( 𝜑 → 𝐾 ∈ Ring )
49 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
50 6 17 49 vr1cl ⊢ ( 𝐾 ∈ Ring → 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
51 48 50 syl ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
52 eqid ⊢ ( ℤRHom ‘ 𝐾 ) = ( ℤRHom ‘ 𝐾 )
53 52 zrhrhm ⊢ ( 𝐾 ∈ Ring → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) )
54 48 53 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) )
55 zringbas ⊢ ℤ = ( Base ‘ ℤring )
56 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
57 55 56 rhmf ⊢ ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
58 54 57 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
59 10 elfzelzd ⊢ ( 𝜑 → 𝑊 ∈ ℤ )
60 58 59 ffvelcdmd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
61 17 14 56 49 ply1sclcl ⊢ ( ( 𝐾 ∈ Ring ∧ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
62 48 60 61 syl2anc ⊢ ( 𝜑 → ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
63 eqid ⊢ ( +g ‘ ( Poly1 ‘ 𝐾 ) ) = ( +g ‘ ( Poly1 ‘ 𝐾 ) )
64 49 63 mndcl ⊢ ( ( ( Poly1 ‘ 𝐾 ) ∈ Mnd ∧ 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
65 46 51 62 64 syl3anc ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
66 22 49 mgpbas ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
67 66 eqcomi ⊢ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
68 26 67 eqtri ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
69 65 68 eleqtrrdi ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( Base ‘ 𝑀 ) )
70 26 7 24 43 69 mulgnn0cld ⊢ ( 𝜑 → ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Base ‘ 𝑀 ) )
71 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
72 22 crngmgp ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ CRing → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ CMnd )
73 19 72 syl ⊢ ( 𝜑 → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ CMnd )
74 15 73 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
75 fzfid ⊢ ( 𝜑 → ( 0 ... 𝐴 ) ∈ Fin )
76 diffi ⊢ ( ( 0 ... 𝐴 ) ∈ Fin → ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ∈ Fin )
77 75 76 syl ⊢ ( 𝜑 → ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ∈ Fin )
78 24 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd )
79 32 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝑌 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
80 eldifi ⊢ ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) → 𝑖 ∈ ( 0 ... 𝐴 ) )
81 80 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝑖 ∈ ( 0 ... 𝐴 ) )
82 79 81 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( 𝑌 ‘ 𝑖 ) ∈ ℕ0 )
83 46 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
84 51 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
85 48 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝐾 ∈ Ring )
86 85 53 57 3syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
87 elfzelz ⊢ ( 𝑖 ∈ ( 0 ... 𝐴 ) → 𝑖 ∈ ℤ )
88 81 87 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → 𝑖 ∈ ℤ )
89 86 88 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝐾 ) )
90 17 14 56 49 ply1sclcl ⊢ ( ( 𝐾 ∈ Ring ∧ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
91 85 89 90 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
92 49 63 mndcl ⊢ ( ( ( Poly1 ‘ 𝐾 ) ∈ Mnd ∧ 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
93 83 84 91 92 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
94 93 68 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑀 ) )
95 26 7 mulgnn0cl ⊢ ( ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd ∧ ( 𝑌 ‘ 𝑖 ) ∈ ℕ0 ∧ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑀 ) )
96 78 82 94 95 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ) → ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑀 ) )
97 96 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑀 ) )
98 71 74 77 97 gsummptcl ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ 𝑀 ) )
99 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
100 71 99 mndcl ⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Base ‘ 𝑀 ) ∧ ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ 𝑀 ) ) → ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ 𝑀 ) )
101 25 70 98 100 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ 𝑀 ) )
102 101 68 eleqtrdi ⊢ ( 𝜑 → ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
103 71 99 cmncom ⊢ ( ( 𝑀 ∈ CMnd ∧ ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Base ‘ 𝑀 ) ∧ ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ 𝑀 ) ) → ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( +g ‘ 𝑀 ) ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
104 74 70 98 103 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( +g ‘ 𝑀 ) ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
105 104 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( +g ‘ 𝑀 ) ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
106 eqid ⊢ ( .r ‘ ( Poly1 ‘ 𝐾 ) ) = ( .r ‘ ( Poly1 ‘ 𝐾 ) )
107 15 106 mgpplusg ⊢ ( .r ‘ ( Poly1 ‘ 𝐾 ) ) = ( +g ‘ 𝑀 )
108 107 eqcomi ⊢ ( +g ‘ 𝑀 ) = ( .r ‘ ( Poly1 ‘ 𝐾 ) )
109 108 a1i ⊢ ( 𝜑 → ( +g ‘ 𝑀 ) = ( .r ‘ ( Poly1 ‘ 𝐾 ) ) )
110 109 oveqd ⊢ ( 𝜑 → ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( +g ‘ 𝑀 ) ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
111 110 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( +g ‘ 𝑀 ) ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
112 98 68 eleqtrdi ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
113 70 68 eleqtrdi ⊢ ( 𝜑 → ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
114 66 7 24 11 65 mulgnn0cld ⊢ ( 𝜑 → ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
115 49 106 21 112 113 114 ringassd ⊢ ( 𝜑 → ( ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) )
116 111 115 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( +g ‘ 𝑀 ) ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) )
117 105 116 eqtrd ⊢ ( 𝜑 → ( ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) )
118 117 oveq2d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) = ( ( 𝐺 ‘ 𝑌 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) ) )
119 37 recnd ⊢ ( 𝜑 → ( 𝑌 ‘ 𝑊 ) ∈ ℂ )
120 38 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
121 119 120 npcand ⊢ ( 𝜑 → ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) + 𝐶 ) = ( 𝑌 ‘ 𝑊 ) )
122 121 eqcomd ⊢ ( 𝜑 → ( 𝑌 ‘ 𝑊 ) = ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) + 𝐶 ) )
123 122 oveq1d ⊢ ( 𝜑 → ( ( 𝑌 ‘ 𝑊 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) = ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) + 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
124 66 a1i ⊢ ( 𝜑 → ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
125 65 124 eleqtrd ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
126 43 11 125 3jca ⊢ ( 𝜑 → ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ∧ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ) )
127 eqid ⊢ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
128 22 106 mgpplusg ⊢ ( .r ‘ ( Poly1 ‘ 𝐾 ) ) = ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
129 127 7 128 mulgnn0dir ⊢ ( ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd ∧ ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ∧ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ) ) → ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) + 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) = ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
130 24 126 129 syl2anc ⊢ ( 𝜑 → ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) + 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) = ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
131 123 130 eqtr2d ⊢ ( 𝜑 → ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( 𝑌 ‘ 𝑊 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
132 131 oveq2d ⊢ ( 𝜑 → ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) = ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( 𝑌 ‘ 𝑊 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
133 8 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) )
134 15 eqcomi ⊢ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) = 𝑀
135 134 a1i ⊢ ( ( 𝜑 ∧ 𝑔 = 𝑌 ) → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) = 𝑀 )
136 simplr ⊢ ( ( ( 𝜑 ∧ 𝑔 = 𝑌 ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑔 = 𝑌 )
137 136 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 = 𝑌 ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑔 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) )
138 14 eqcomi ⊢ ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) = 𝑆
139 138 a1i ⊢ ( ( ( 𝜑 ∧ 𝑔 = 𝑌 ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) = 𝑆 )
140 139 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 = 𝑌 ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) = ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) )
141 140 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑔 = 𝑌 ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) = ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) )
142 137 141 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑔 = 𝑌 ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) = ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) )
143 142 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑔 = 𝑌 ) → ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) = ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) )
144 135 143 oveq12d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝑌 ) → ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) = ( 𝑀 Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
145 ovexd ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ V )
146 133 144 9 145 fvmptd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) = ( 𝑀 Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
147 10 snssd ⊢ ( 𝜑 → { 𝑊 } ⊆ ( 0 ... 𝐴 ) )
148 undifr ⊢ ( { 𝑊 } ⊆ ( 0 ... 𝐴 ) ↔ ( ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ∪ { 𝑊 } ) = ( 0 ... 𝐴 ) )
149 147 148 sylib ⊢ ( 𝜑 → ( ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ∪ { 𝑊 } ) = ( 0 ... 𝐴 ) )
150 149 eqcomd ⊢ ( 𝜑 → ( 0 ... 𝐴 ) = ( ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ∪ { 𝑊 } ) )
151 150 mpteq1d ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) = ( 𝑖 ∈ ( ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ∪ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) )
152 151 oveq2d ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) = ( 𝑀 Σg ( 𝑖 ∈ ( ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ∪ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
153 146 152 eqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) = ( 𝑀 Σg ( 𝑖 ∈ ( ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ∪ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
154 neldifsnd ⊢ ( 𝜑 → ¬ 𝑊 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) )
155 26 7 24 33 69 mulgnn0cld ⊢ ( 𝜑 → ( ( 𝑌 ‘ 𝑊 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Base ‘ 𝑀 ) )
156 fveq2 ⊢ ( 𝑖 = 𝑊 → ( 𝑌 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑊 ) )
157 2fveq3 ⊢ ( 𝑖 = 𝑊 → ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) = ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) )
158 157 oveq2d ⊢ ( 𝑖 = 𝑊 → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) = ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
159 156 158 oveq12d ⊢ ( 𝑖 = 𝑊 → ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) = ( ( 𝑌 ‘ 𝑊 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
160 71 107 74 77 96 10 154 155 159 gsumunsn ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑖 ∈ ( ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ∪ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) = ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( 𝑌 ‘ 𝑊 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
161 153 160 eqtr2d ⊢ ( 𝜑 → ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( 𝑌 ‘ 𝑊 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( 𝐺 ‘ 𝑌 ) )
162 132 161 eqtrd ⊢ ( 𝜑 → ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) = ( 𝐺 ‘ 𝑌 ) )
163 162 oveq2d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) ) = ( ( 𝐺 ‘ 𝑌 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑌 ) ) )
164 21 ringgrpd ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Grp )
165 1 2 3 4 5 6 7 8 aks6d1c5lem0 ⊢ ( 𝜑 → 𝐺 : ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
166 165 9 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
167 eqid ⊢ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) = ( 0g ‘ ( Poly1 ‘ 𝐾 ) )
168 eqid ⊢ ( -g ‘ ( Poly1 ‘ 𝐾 ) ) = ( -g ‘ ( Poly1 ‘ 𝐾 ) )
169 49 167 168 grpsubid ⊢ ( ( ( Poly1 ‘ 𝐾 ) ∈ Grp ∧ ( 𝐺 ‘ 𝑌 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) → ( ( 𝐺 ‘ 𝑌 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑌 ) ) = ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) )
170 164 166 169 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐺 ‘ 𝑌 ) ) = ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) )
171 163 170 eqtrd ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) ) = ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) )
172 118 171 eqtrd ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) = ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) )
173 172 fveq2d ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑌 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) ) = ( ( deg1 ‘ 𝐾 ) ‘ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ) )
174 eqid ⊢ ( deg1 ‘ 𝐾 ) = ( deg1 ‘ 𝐾 )
175 174 17 167 deg1z ⊢ ( 𝐾 ∈ Ring → ( ( deg1 ‘ 𝐾 ) ‘ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ) = -∞ )
176 48 175 syl ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ) = -∞ )
177 1 flddrngd ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
178 drngdomn ⊢ ( 𝐾 ∈ DivRing → 𝐾 ∈ Domn )
179 177 178 syl ⊢ ( 𝜑 → 𝐾 ∈ Domn )
180 17 ply1domn ⊢ ( 𝐾 ∈ Domn → ( Poly1 ‘ 𝐾 ) ∈ Domn )
181 179 180 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Domn )
182 19 181 jca ⊢ ( 𝜑 → ( ( Poly1 ‘ 𝐾 ) ∈ CRing ∧ ( Poly1 ‘ 𝐾 ) ∈ Domn ) )
183 isidom ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ IDomn ↔ ( ( Poly1 ‘ 𝐾 ) ∈ CRing ∧ ( Poly1 ‘ 𝐾 ) ∈ Domn ) )
184 182 183 sylibr ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ IDomn )
185 174 17 49 deg1xrcl ⊢ ( ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ℝ* )
186 62 185 syl ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ℝ* )
187 0xr ⊢ 0 ∈ ℝ*
188 187 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
189 174 17 49 deg1xrcl ⊢ ( 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) ∈ ℝ* )
190 51 189 syl ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) ∈ ℝ* )
191 174 17 56 14 deg1sclle ⊢ ( ( 𝐾 ∈ Ring ∧ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ≤ 0 )
192 48 60 191 syl2anc ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ≤ 0 )
193 0lt1 ⊢ 0 < 1
194 193 a1i ⊢ ( 𝜑 → 0 < 1 )
195 51 66 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
196 127 7 mulg1 ⊢ ( 𝑋 ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) → ( 1 ↑ 𝑋 ) = 𝑋 )
197 195 196 syl ⊢ ( 𝜑 → ( 1 ↑ 𝑋 ) = 𝑋 )
198 197 fveq2d ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 1 ↑ 𝑋 ) ) = ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) )
199 isfld ⊢ ( 𝐾 ∈ Field ↔ ( 𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing ) )
200 199 biimpi ⊢ ( 𝐾 ∈ Field → ( 𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing ) )
201 1 200 syl ⊢ ( 𝜑 → ( 𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing ) )
202 201 simpld ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
203 drngnzr ⊢ ( 𝐾 ∈ DivRing → 𝐾 ∈ NzRing )
204 202 203 syl ⊢ ( 𝜑 → 𝐾 ∈ NzRing )
205 1nn0 ⊢ 1 ∈ ℕ0
206 205 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
207 174 17 6 22 7 deg1pw ⊢ ( ( 𝐾 ∈ NzRing ∧ 1 ∈ ℕ0 ) → ( ( deg1 ‘ 𝐾 ) ‘ ( 1 ↑ 𝑋 ) ) = 1 )
208 204 206 207 syl2anc ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 1 ↑ 𝑋 ) ) = 1 )
209 198 208 eqtr3d ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) = 1 )
210 209 eqcomd ⊢ ( 𝜑 → 1 = ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) )
211 194 210 breqtrd ⊢ ( 𝜑 → 0 < ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) )
212 186 188 190 192 211 xrlelttrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) < ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) )
213 17 174 48 49 63 51 62 212 deg1add ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) = ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) )
214 209 206 eqeltrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) ∈ ℕ0 )
215 213 214 eqeltrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ℕ0 )
216 174 17 167 49 deg1nn0clb ⊢ ( ( 𝐾 ∈ Ring ∧ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) → ( ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ↔ ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ℕ0 ) )
217 48 65 216 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ↔ ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ℕ0 ) )
218 215 217 mpbird ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) )
219 184 65 218 11 7 idomnnzpownz ⊢ ( 𝜑 → ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) )
220 174 17 167 49 deg1nn0clb ⊢ ( ( 𝐾 ∈ Ring ∧ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) → ( ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ↔ ( ( deg1 ‘ 𝐾 ) ‘ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ∈ ℕ0 ) )
221 48 114 220 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ↔ ( ( deg1 ‘ 𝐾 ) ‘ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ∈ ℕ0 ) )
222 219 221 mpbid ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ∈ ℕ0 )
223 222 nn0red ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ∈ ℝ )
224 223 mnfltd ⊢ ( 𝜑 → -∞ < ( ( deg1 ‘ 𝐾 ) ‘ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
225 176 224 eqbrtrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ) < ( ( deg1 ‘ 𝐾 ) ‘ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
226 173 225 eqbrtrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑌 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) ) < ( ( deg1 ‘ 𝐾 ) ‘ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) )
227 102 226 jca ⊢ ( 𝜑 → ( ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑌 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) ) < ( ( deg1 ‘ 𝐾 ) ‘ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) )
228 eqid ⊢ ( Unic1p ‘ 𝐾 ) = ( Unic1p ‘ 𝐾 )
229 17 49 167 228 drnguc1p ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐾 ) ) ) → ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Unic1p ‘ 𝐾 ) )
230 177 114 219 229 syl3anc ⊢ ( 𝜑 → ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Unic1p ‘ 𝐾 ) )
231 13 17 49 174 168 106 228 q1peqb ⊢ ( ( 𝐾 ∈ Ring ∧ ( 𝐺 ‘ 𝑌 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( Unic1p ‘ 𝐾 ) ) → ( ( ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑌 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) ) < ( ( deg1 ‘ 𝐾 ) ‘ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) ↔ ( ( 𝐺 ‘ 𝑌 ) 𝑄 ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) )
232 48 166 230 231 syl3anc ⊢ ( 𝜑 → ( ( ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( deg1 ‘ 𝐾 ) ‘ ( ( 𝐺 ‘ 𝑌 ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ( .r ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) ) < ( ( deg1 ‘ 𝐾 ) ‘ ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ) ↔ ( ( 𝐺 ‘ 𝑌 ) 𝑄 ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) ) )
233 227 232 mpbid ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) 𝑄 ( 𝐶 ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) = ( ( ( ( 𝑌 ‘ 𝑊 ) − 𝐶 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑖 ∈ ( ( 0 ... 𝐴 ) ∖ { 𝑊 } ) ↦ ( ( 𝑌 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑆 ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ) )