Metamath Proof Explorer


Theorem vietalem

Description: Lemma for vieta : induction step. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses vieta.w 𝑊 = ( Poly1𝑅 )
vieta.b 𝐵 = ( Base ‘ 𝑅 )
vieta.3 = ( -g𝑊 )
vieta.m 𝑀 = ( mulGrp ‘ 𝑊 )
vieta.q 𝑄 = ( 𝐼 eval 𝑅 )
vieta.e 𝐸 = ( 𝐼 eSymPoly 𝑅 )
vieta.n 𝑁 = ( invg𝑅 )
vieta.1 1 = ( 1r𝑅 )
vieta.t · = ( .r𝑅 )
vieta.x 𝑋 = ( var1𝑅 )
vieta.a 𝐴 = ( algSc ‘ 𝑊 )
vieta.p = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
vieta.h 𝐻 = ( ♯ ‘ 𝐼 )
vieta.i ( 𝜑𝐼 ∈ Fin )
vieta.r ( 𝜑𝑅 ∈ IDomn )
vieta.z ( 𝜑𝑍 : 𝐼𝐵 )
vieta.f 𝐹 = ( 𝑀 Σg ( 𝑛𝐼 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) )
vieta.k ( 𝜑𝐾 ∈ ( 0 ... 𝐻 ) )
vietalem.y ( 𝜑𝑌𝐼 )
vietalem.j 𝐽 = ( 𝐼 ∖ { 𝑌 } )
vietalem.2 ( 𝜑 → ∀ 𝑧 ∈ ( 𝐵m 𝐽 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑧𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) = ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
vietalem.3 ( 𝜑 → ( ( deg1𝑅 ) ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) = ( ♯ ‘ 𝐽 ) )
Assertion vietalem ( 𝜑 → ( ( coe1𝐹 ) ‘ 𝐾 ) = ( ( ( 𝐻𝐾 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝐾 ) ) ) ‘ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 vieta.w 𝑊 = ( Poly1𝑅 )
2 vieta.b 𝐵 = ( Base ‘ 𝑅 )
3 vieta.3 = ( -g𝑊 )
4 vieta.m 𝑀 = ( mulGrp ‘ 𝑊 )
5 vieta.q 𝑄 = ( 𝐼 eval 𝑅 )
6 vieta.e 𝐸 = ( 𝐼 eSymPoly 𝑅 )
7 vieta.n 𝑁 = ( invg𝑅 )
8 vieta.1 1 = ( 1r𝑅 )
9 vieta.t · = ( .r𝑅 )
10 vieta.x 𝑋 = ( var1𝑅 )
11 vieta.a 𝐴 = ( algSc ‘ 𝑊 )
12 vieta.p = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
13 vieta.h 𝐻 = ( ♯ ‘ 𝐼 )
14 vieta.i ( 𝜑𝐼 ∈ Fin )
15 vieta.r ( 𝜑𝑅 ∈ IDomn )
16 vieta.z ( 𝜑𝑍 : 𝐼𝐵 )
17 vieta.f 𝐹 = ( 𝑀 Σg ( 𝑛𝐼 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) )
18 vieta.k ( 𝜑𝐾 ∈ ( 0 ... 𝐻 ) )
19 vietalem.y ( 𝜑𝑌𝐼 )
20 vietalem.j 𝐽 = ( 𝐼 ∖ { 𝑌 } )
21 vietalem.2 ( 𝜑 → ∀ 𝑧 ∈ ( 𝐵m 𝐽 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑧𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) = ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
22 vietalem.3 ( 𝜑 → ( ( deg1𝑅 ) ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) = ( ♯ ‘ 𝐽 ) )
23 17 a1i ( 𝜑𝐹 = ( 𝑀 Σg ( 𝑛𝐼 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) ) )
24 20 uneq1i ( 𝐽 ∪ { 𝑌 } ) = ( ( 𝐼 ∖ { 𝑌 } ) ∪ { 𝑌 } )
25 19 snssd ( 𝜑 → { 𝑌 } ⊆ 𝐼 )
26 undifr ( { 𝑌 } ⊆ 𝐼 ↔ ( ( 𝐼 ∖ { 𝑌 } ) ∪ { 𝑌 } ) = 𝐼 )
27 25 26 sylib ( 𝜑 → ( ( 𝐼 ∖ { 𝑌 } ) ∪ { 𝑌 } ) = 𝐼 )
28 24 27 eqtr2id ( 𝜑𝐼 = ( 𝐽 ∪ { 𝑌 } ) )
29 28 mpteq1d ( 𝜑 → ( 𝑛𝐼 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) = ( 𝑛 ∈ ( 𝐽 ∪ { 𝑌 } ) ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) )
30 29 oveq2d ( 𝜑 → ( 𝑀 Σg ( 𝑛𝐼 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) ) = ( 𝑀 Σg ( 𝑛 ∈ ( 𝐽 ∪ { 𝑌 } ) ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) ) )
31 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
32 4 31 mgpbas ( Base ‘ 𝑊 ) = ( Base ‘ 𝑀 )
33 eqid ( .r𝑊 ) = ( .r𝑊 )
34 4 33 mgpplusg ( .r𝑊 ) = ( +g𝑀 )
35 15 idomcringd ( 𝜑𝑅 ∈ CRing )
36 1 ply1crng ( 𝑅 ∈ CRing → 𝑊 ∈ CRing )
37 4 crngmgp ( 𝑊 ∈ CRing → 𝑀 ∈ CMnd )
38 35 36 37 3syl ( 𝜑𝑀 ∈ CMnd )
39 diffi ( 𝐼 ∈ Fin → ( 𝐼 ∖ { 𝑌 } ) ∈ Fin )
40 14 39 syl ( 𝜑 → ( 𝐼 ∖ { 𝑌 } ) ∈ Fin )
41 20 40 eqeltrid ( 𝜑𝐽 ∈ Fin )
42 35 36 syl ( 𝜑𝑊 ∈ CRing )
43 42 crngringd ( 𝜑𝑊 ∈ Ring )
44 43 ringgrpd ( 𝜑𝑊 ∈ Grp )
45 44 adantr ( ( 𝜑𝑛𝐽 ) → 𝑊 ∈ Grp )
46 15 idomringd ( 𝜑𝑅 ∈ Ring )
47 10 1 31 vr1cl ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑊 ) )
48 46 47 syl ( 𝜑𝑋 ∈ ( Base ‘ 𝑊 ) )
49 48 adantr ( ( 𝜑𝑛𝐽 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
50 eqid ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
51 eqid ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
52 1 ply1assa ( 𝑅 ∈ CRing → 𝑊 ∈ AssAlg )
53 35 52 syl ( 𝜑𝑊 ∈ AssAlg )
54 53 adantr ( ( 𝜑𝑛𝐽 ) → 𝑊 ∈ AssAlg )
55 16 adantr ( ( 𝜑𝑛𝐽 ) → 𝑍 : 𝐼𝐵 )
56 difss ( 𝐼 ∖ { 𝑌 } ) ⊆ 𝐼
57 20 56 eqsstri 𝐽𝐼
58 57 a1i ( 𝜑𝐽𝐼 )
59 58 sselda ( ( 𝜑𝑛𝐽 ) → 𝑛𝐼 )
60 55 59 ffvelcdmd ( ( 𝜑𝑛𝐽 ) → ( 𝑍𝑛 ) ∈ 𝐵 )
61 1 ply1sca ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑊 ) )
62 35 61 syl ( 𝜑𝑅 = ( Scalar ‘ 𝑊 ) )
63 62 fveq2d ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
64 2 63 eqtrid ( 𝜑𝐵 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
65 64 adantr ( ( 𝜑𝑛𝐽 ) → 𝐵 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
66 60 65 eleqtrd ( ( 𝜑𝑛𝐽 ) → ( 𝑍𝑛 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
67 11 50 51 54 66 asclelbas ( ( 𝜑𝑛𝐽 ) → ( 𝐴 ‘ ( 𝑍𝑛 ) ) ∈ ( Base ‘ 𝑊 ) )
68 31 3 45 49 67 grpsubcld ( ( 𝜑𝑛𝐽 ) → ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ∈ ( Base ‘ 𝑊 ) )
69 neldifsnd ( 𝜑 → ¬ 𝑌 ∈ ( 𝐼 ∖ { 𝑌 } ) )
70 20 eleq2i ( 𝑌𝐽𝑌 ∈ ( 𝐼 ∖ { 𝑌 } ) )
71 69 70 sylnibr ( 𝜑 → ¬ 𝑌𝐽 )
72 64 16 feq3dd ( 𝜑𝑍 : 𝐼 ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
73 72 19 ffvelcdmd ( 𝜑 → ( 𝑍𝑌 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
74 11 50 51 53 73 asclelbas ( 𝜑 → ( 𝐴 ‘ ( 𝑍𝑌 ) ) ∈ ( Base ‘ 𝑊 ) )
75 31 3 44 48 74 grpsubcld ( 𝜑 → ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) ∈ ( Base ‘ 𝑊 ) )
76 2fveq3 ( 𝑛 = 𝑌 → ( 𝐴 ‘ ( 𝑍𝑛 ) ) = ( 𝐴 ‘ ( 𝑍𝑌 ) ) )
77 76 oveq2d ( 𝑛 = 𝑌 → ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) = ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) )
78 32 34 38 41 68 19 71 75 77 gsumunsn ( 𝜑 → ( 𝑀 Σg ( 𝑛 ∈ ( 𝐽 ∪ { 𝑌 } ) ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) ) = ( ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) ) ( .r𝑊 ) ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) ) )
79 23 30 78 3eqtrd ( 𝜑𝐹 = ( ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) ) ( .r𝑊 ) ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) ) )
80 eqid ( ·𝑠𝑊 ) = ( ·𝑠𝑊 )
81 eqid ( .g𝑀 ) = ( .g𝑀 )
82 eqid ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) = ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) )
83 eqid ( ( deg1𝑅 ) ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) = ( ( deg1𝑅 ) ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) )
84 simpr ( ( 𝜑𝑛𝐽 ) → 𝑛𝐽 )
85 84 fvresd ( ( 𝜑𝑛𝐽 ) → ( ( 𝑍𝐽 ) ‘ 𝑛 ) = ( 𝑍𝑛 ) )
86 85 fveq2d ( ( 𝜑𝑛𝐽 ) → ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) = ( 𝐴 ‘ ( 𝑍𝑛 ) ) )
87 86 oveq2d ( ( 𝜑𝑛𝐽 ) → ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) = ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) )
88 87 mpteq2dva ( 𝜑 → ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) = ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) )
89 88 oveq2d ( 𝜑 → ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) = ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) ) )
90 68 ralrimiva ( 𝜑 → ∀ 𝑛𝐽 ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ∈ ( Base ‘ 𝑊 ) )
91 32 38 41 90 gsummptcl ( 𝜑 → ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) ) ∈ ( Base ‘ 𝑊 ) )
92 89 91 eqeltrd ( 𝜑 → ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ∈ ( Base ‘ 𝑊 ) )
93 1 10 31 80 4 81 82 83 46 92 ply1coedeg ( 𝜑 → ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ( deg1𝑅 ) ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ) ↦ ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ 𝑙 ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) )
94 22 oveq2d ( 𝜑 → ( 0 ... ( ( deg1𝑅 ) ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ) = ( 0 ... ( ♯ ‘ 𝐽 ) ) )
95 94 mpteq1d ( 𝜑 → ( 𝑙 ∈ ( 0 ... ( ( deg1𝑅 ) ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ) ↦ ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ 𝑙 ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) = ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ 𝑙 ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) )
96 95 oveq2d ( 𝜑 → ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ( deg1𝑅 ) ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ) ↦ ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ 𝑙 ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ 𝑙 ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) )
97 93 89 96 3eqtr3d ( 𝜑 → ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ 𝑙 ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) )
98 43 ringcmnd ( 𝜑𝑊 ∈ CMnd )
99 hashcl ( 𝐽 ∈ Fin → ( ♯ ‘ 𝐽 ) ∈ ℕ0 )
100 41 99 syl ( 𝜑 → ( ♯ ‘ 𝐽 ) ∈ ℕ0 )
101 1 ply1lmod ( 𝑅 ∈ Ring → 𝑊 ∈ LMod )
102 46 101 syl ( 𝜑𝑊 ∈ LMod )
103 102 adantr ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑊 ∈ LMod )
104 92 adantr ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ∈ ( Base ‘ 𝑊 ) )
105 62 fveq2d ( 𝜑 → ( Poly1𝑅 ) = ( Poly1 ‘ ( Scalar ‘ 𝑊 ) ) )
106 1 105 eqtrid ( 𝜑𝑊 = ( Poly1 ‘ ( Scalar ‘ 𝑊 ) ) )
107 106 fveq2d ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ ( Poly1 ‘ ( Scalar ‘ 𝑊 ) ) ) )
108 107 adantr ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( Base ‘ 𝑊 ) = ( Base ‘ ( Poly1 ‘ ( Scalar ‘ 𝑊 ) ) ) )
109 104 108 eleqtrd ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ( Scalar ‘ 𝑊 ) ) ) )
110 fz0ssnn0 ( 0 ... ( ♯ ‘ 𝐽 ) ) ⊆ ℕ0
111 simpr ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
112 110 111 sselid ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑙 ∈ ℕ0 )
113 eqid ( Base ‘ ( Poly1 ‘ ( Scalar ‘ 𝑊 ) ) ) = ( Base ‘ ( Poly1 ‘ ( Scalar ‘ 𝑊 ) ) )
114 eqid ( Poly1 ‘ ( Scalar ‘ 𝑊 ) ) = ( Poly1 ‘ ( Scalar ‘ 𝑊 ) )
115 82 113 114 51 coe1fvalcl ( ( ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑙 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ 𝑙 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
116 109 112 115 syl2anc ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ 𝑙 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
117 38 cmnmndd ( 𝜑𝑀 ∈ Mnd )
118 117 adantr ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑀 ∈ Mnd )
119 46 adantr ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑅 ∈ Ring )
120 119 47 syl ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
121 32 81 118 112 120 mulgnn0cld ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑙 ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
122 31 50 80 51 103 116 121 lmodvscld ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ 𝑙 ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) )
123 simpr ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) )
124 123 fveq2d ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ 𝑙 ) = ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) )
125 oveq1 ( 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) → ( 𝑙 ( .g𝑀 ) 𝑋 ) = ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) )
126 125 adantl ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( 𝑙 ( .g𝑀 ) 𝑋 ) = ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) )
127 124 126 oveq12d ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ 𝑙 ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) = ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) )
128 31 98 100 122 127 gsummptrev ( 𝜑 → ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ 𝑙 ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) = ( 𝑊 Σg ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) ) )
129 fveq1 ( 𝑧 = ( 𝑍𝐽 ) → ( 𝑧𝑛 ) = ( ( 𝑍𝐽 ) ‘ 𝑛 ) )
130 129 fveq2d ( 𝑧 = ( 𝑍𝐽 ) → ( 𝐴 ‘ ( 𝑧𝑛 ) ) = ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) )
131 130 oveq2d ( 𝑧 = ( 𝑍𝐽 ) → ( 𝑋 ( 𝐴 ‘ ( 𝑧𝑛 ) ) ) = ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) )
132 131 mpteq2dv ( 𝑧 = ( 𝑍𝐽 ) → ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑧𝑛 ) ) ) ) = ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) )
133 132 oveq2d ( 𝑧 = ( 𝑍𝐽 ) → ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑧𝑛 ) ) ) ) ) = ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) )
134 133 fveq2d ( 𝑧 = ( 𝑍𝐽 ) → ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑧𝑛 ) ) ) ) ) ) = ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) )
135 134 fveq1d ( 𝑧 = ( 𝑍𝐽 ) → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑧𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) = ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) )
136 fveq2 ( 𝑧 = ( 𝑍𝐽 ) → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) = ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) )
137 136 oveq2d ( 𝑧 = ( 𝑍𝐽 ) → ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) )
138 135 137 eqeq12d ( 𝑧 = ( 𝑍𝐽 ) → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑧𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) = ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) = ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) )
139 138 ralbidv ( 𝑧 = ( 𝑍𝐽 ) → ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑧𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) = ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) = ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) )
140 2 fvexi 𝐵 ∈ V
141 140 a1i ( 𝜑𝐵 ∈ V )
142 16 58 fssresd ( 𝜑 → ( 𝑍𝐽 ) : 𝐽𝐵 )
143 141 41 142 elmapdd ( 𝜑 → ( 𝑍𝐽 ) ∈ ( 𝐵m 𝐽 ) )
144 139 21 143 rspcdva ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) = ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) )
145 144 r19.21bi ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) = ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) )
146 145 oveq1d ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) )
147 146 mpteq2dva ( 𝜑 → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) = ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) )
148 147 oveq2d ( 𝜑 → ( 𝑊 Σg ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) ) = ( 𝑊 Σg ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) ) )
149 eqid ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
150 149 2 mgpbas 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
151 149 ringmgp ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
152 119 151 syl ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
153 fznn0sub2 ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
154 153 adantl ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
155 110 154 sselid ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ∈ ℕ0 )
156 46 ringgrpd ( 𝜑𝑅 ∈ Grp )
157 2 8 46 ringidcld ( 𝜑1𝐵 )
158 2 7 156 157 grpinvcld ( 𝜑 → ( 𝑁1 ) ∈ 𝐵 )
159 158 adantr ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑁1 ) ∈ 𝐵 )
160 150 12 152 155 159 mulgnn0cld ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) ∈ 𝐵 )
161 eqid ( 𝐽 eval 𝑅 ) = ( 𝐽 eval 𝑅 )
162 eqid ( 𝐽 mPoly 𝑅 ) = ( 𝐽 mPoly 𝑅 )
163 eqid ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
164 41 adantr ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝐽 ∈ Fin )
165 35 adantr ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑅 ∈ CRing )
166 eqid { ∈ ( ℕ0m 𝐽 ) ∣ finSupp 0 } = { ∈ ( ℕ0m 𝐽 ) ∣ finSupp 0 }
167 166 164 119 155 163 esplympl ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
168 143 adantr ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑍𝐽 ) ∈ ( 𝐵m 𝐽 ) )
169 161 162 163 2 164 165 167 168 evlcl ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ∈ 𝐵 )
170 2 9 119 160 169 ringcld ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ 𝐵 )
171 1 31 2 80 119 170 121 ply1vscl ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) )
172 100 nn0cnd ( 𝜑 → ( ♯ ‘ 𝐽 ) ∈ ℂ )
173 172 ad2antrr ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ♯ ‘ 𝐽 ) ∈ ℂ )
174 simplr ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
175 110 174 sselid ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → 𝑘 ∈ ℕ0 )
176 175 nn0cnd ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → 𝑘 ∈ ℂ )
177 173 176 subcld ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ∈ ℂ )
178 123 177 eqeltrd ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → 𝑙 ∈ ℂ )
179 173 178 subcld ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ∈ ℂ )
180 173 178 nncand ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ( ♯ ‘ 𝐽 ) − ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) = 𝑙 )
181 180 123 eqtrd ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ( ♯ ‘ 𝐽 ) − ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) )
182 173 179 176 181 subcand ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑙 ) = 𝑘 )
183 182 oveq1d ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) = ( 𝑘 ( 𝑁1 ) ) )
184 182 fveq2d ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) = ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) )
185 184 fveq2d ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) = ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) )
186 185 fveq1d ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) = ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) )
187 183 186 oveq12d ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) = ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) )
188 187 126 oveq12d ( ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) → ( ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) = ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) )
189 31 98 100 171 188 gsummptrev ( 𝜑 → ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) = ( 𝑊 Σg ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) ) )
190 148 189 eqtr4d ( 𝜑 → ( 𝑊 Σg ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( ( 𝑍𝐽 ) ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) )
191 97 128 190 3eqtrd ( 𝜑 → ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) )
192 191 oveq1d ( 𝜑 → ( ( 𝑀 Σg ( 𝑛𝐽 ↦ ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑛 ) ) ) ) ) ( .r𝑊 ) ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) ) = ( ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) ( .r𝑊 ) ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) ) )
193 eqid ( +g𝑊 ) = ( +g𝑊 )
194 46 adantr ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑅 ∈ Ring )
195 194 151 syl ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
196 elfznn0 ( 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) → 𝑖 ∈ ℕ0 )
197 196 adantl ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑖 ∈ ℕ0 )
198 158 adantr ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑁1 ) ∈ 𝐵 )
199 150 12 195 197 198 mulgnn0cld ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑖 ( 𝑁1 ) ) ∈ 𝐵 )
200 41 adantr ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝐽 ∈ Fin )
201 35 adantr ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑅 ∈ CRing )
202 166 200 194 197 163 esplympl ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
203 143 adantr ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑍𝐽 ) ∈ ( 𝐵m 𝐽 ) )
204 161 162 163 2 200 201 202 203 evlcl ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) ∈ 𝐵 )
205 2 9 194 199 204 ringcld ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑖 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ 𝐵 )
206 117 adantr ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑀 ∈ Mnd )
207 fznn0sub2 ( 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑖 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
208 207 adantl ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑖 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
209 110 208 sselid ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑖 ) ∈ ℕ0 )
210 48 adantr ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
211 32 81 206 209 210 mulgnn0cld ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ♯ ‘ 𝐽 ) − 𝑖 ) ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
212 1 31 2 80 194 205 211 ply1vscl ( ( 𝜑𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑖 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑖 ) ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) )
213 oveq1 ( 𝑖 = 0 → ( 𝑖 ( 𝑁1 ) ) = ( 0 ( 𝑁1 ) ) )
214 2fveq3 ( 𝑖 = 0 → ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) = ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) )
215 214 fveq1d ( 𝑖 = 0 → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) = ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) )
216 213 215 oveq12d ( 𝑖 = 0 → ( ( 𝑖 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) ) = ( ( 0 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) ) )
217 oveq2 ( 𝑖 = 0 → ( ( ♯ ‘ 𝐽 ) − 𝑖 ) = ( ( ♯ ‘ 𝐽 ) − 0 ) )
218 217 oveq1d ( 𝑖 = 0 → ( ( ( ♯ ‘ 𝐽 ) − 𝑖 ) ( .g𝑀 ) 𝑋 ) = ( ( ( ♯ ‘ 𝐽 ) − 0 ) ( .g𝑀 ) 𝑋 ) )
219 216 218 oveq12d ( 𝑖 = 0 → ( ( ( 𝑖 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑖 ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( 0 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 0 ) ( .g𝑀 ) 𝑋 ) ) )
220 oveq1 ( 𝑖 = ( ♯ ‘ 𝐽 ) → ( 𝑖 ( 𝑁1 ) ) = ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) )
221 2fveq3 ( 𝑖 = ( ♯ ‘ 𝐽 ) → ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) = ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) )
222 221 fveq1d ( 𝑖 = ( ♯ ‘ 𝐽 ) → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) = ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) )
223 220 222 oveq12d ( 𝑖 = ( ♯ ‘ 𝐽 ) → ( ( 𝑖 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) ) = ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) )
224 oveq2 ( 𝑖 = ( ♯ ‘ 𝐽 ) → ( ( ♯ ‘ 𝐽 ) − 𝑖 ) = ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) )
225 224 oveq1d ( 𝑖 = ( ♯ ‘ 𝐽 ) → ( ( ( ♯ ‘ 𝐽 ) − 𝑖 ) ( .g𝑀 ) 𝑋 ) = ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) )
226 223 225 oveq12d ( 𝑖 = ( ♯ ‘ 𝐽 ) → ( ( ( 𝑖 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑖 ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) )
227 oveq1 ( 𝑖 = 𝑘 → ( 𝑖 ( 𝑁1 ) ) = ( 𝑘 ( 𝑁1 ) ) )
228 2fveq3 ( 𝑖 = 𝑘 → ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) = ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) )
229 228 fveq1d ( 𝑖 = 𝑘 → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) = ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) )
230 227 229 oveq12d ( 𝑖 = 𝑘 → ( ( 𝑖 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) ) = ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) )
231 oveq2 ( 𝑖 = 𝑘 → ( ( ♯ ‘ 𝐽 ) − 𝑖 ) = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) )
232 231 oveq1d ( 𝑖 = 𝑘 → ( ( ( ♯ ‘ 𝐽 ) − 𝑖 ) ( .g𝑀 ) 𝑋 ) = ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) )
233 230 232 oveq12d ( 𝑖 = 𝑘 → ( ( ( 𝑖 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑖 ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) )
234 oveq1 ( 𝑖 = ( 𝑘 + 1 ) → ( 𝑖 ( 𝑁1 ) ) = ( ( 𝑘 + 1 ) ( 𝑁1 ) ) )
235 2fveq3 ( 𝑖 = ( 𝑘 + 1 ) → ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) = ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) )
236 235 fveq1d ( 𝑖 = ( 𝑘 + 1 ) → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) = ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) )
237 234 236 oveq12d ( 𝑖 = ( 𝑘 + 1 ) → ( ( 𝑖 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) ) = ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) )
238 oveq2 ( 𝑖 = ( 𝑘 + 1 ) → ( ( ♯ ‘ 𝐽 ) − 𝑖 ) = ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) )
239 238 oveq1d ( 𝑖 = ( 𝑘 + 1 ) → ( ( ( ♯ ‘ 𝐽 ) − 𝑖 ) ( .g𝑀 ) 𝑋 ) = ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) )
240 237 239 oveq12d ( 𝑖 = ( 𝑘 + 1 ) → ( ( ( 𝑖 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑖 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑖 ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) )
241 eqid ( invg𝑊 ) = ( invg𝑊 )
242 46 151 syl ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
243 0nn0 0 ∈ ℕ0
244 243 a1i ( 𝜑 → 0 ∈ ℕ0 )
245 150 12 242 244 158 mulgnn0cld ( 𝜑 → ( 0 ( 𝑁1 ) ) ∈ 𝐵 )
246 8 157 eqeltrrid ( 𝜑 → ( 1r𝑅 ) ∈ 𝐵 )
247 2 9 46 245 246 ringcld ( 𝜑 → ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ∈ 𝐵 )
248 hashcl ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
249 14 248 syl ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
250 13 249 eqeltrid ( 𝜑𝐻 ∈ ℕ0 )
251 32 81 117 250 48 mulgnn0cld ( 𝜑 → ( 𝐻 ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
252 1 31 2 80 46 247 251 ply1vscl ( 𝜑 → ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) )
253 150 12 242 250 158 mulgnn0cld ( 𝜑 → ( 𝐻 ( 𝑁1 ) ) ∈ 𝐵 )
254 eqid ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
255 eqid ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
256 6 fveq1i ( 𝐸𝐻 ) = ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐻 )
257 eqid { ∈ ( ℕ0m 𝐼 ) ∣ finSupp 0 } = { ∈ ( ℕ0m 𝐼 ) ∣ finSupp 0 }
258 257 14 46 250 255 esplympl ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐻 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
259 256 258 eqeltrid ( 𝜑 → ( 𝐸𝐻 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
260 141 14 16 elmapdd ( 𝜑𝑍 ∈ ( 𝐵m 𝐼 ) )
261 5 254 255 2 14 35 259 260 evlcl ( 𝜑 → ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ∈ 𝐵 )
262 2 9 46 253 261 ringcld ( 𝜑 → ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ∈ 𝐵 )
263 32 81 117 244 48 mulgnn0cld ( 𝜑 → ( 0 ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
264 1 31 2 80 46 262 263 ply1vscl ( 𝜑 → ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) )
265 31 193 3 241 44 252 264 grpsubinv ( 𝜑 → ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( ( invg𝑊 ) ‘ ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) ) = ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) )
266 166 41 46 244 163 esplympl ( 𝜑 → ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
267 161 162 163 2 41 35 266 143 evlcl ( 𝜑 → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) ∈ 𝐵 )
268 2 9 46 245 267 ringcld ( 𝜑 → ( ( 0 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ 𝐵 )
269 268 64 eleqtrd ( 𝜑 → ( ( 0 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
270 172 subid1d ( 𝜑 → ( ( ♯ ‘ 𝐽 ) − 0 ) = ( ♯ ‘ 𝐽 ) )
271 270 100 eqeltrd ( 𝜑 → ( ( ♯ ‘ 𝐽 ) − 0 ) ∈ ℕ0 )
272 32 81 117 271 48 mulgnn0cld ( 𝜑 → ( ( ( ♯ ‘ 𝐽 ) − 0 ) ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
273 31 50 51 80 33 53 269 272 48 assaassd ( 𝜑 → ( ( ( ( 0 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 0 ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) 𝑋 ) = ( ( ( 0 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ( ♯ ‘ 𝐽 ) − 0 ) ( .g𝑀 ) 𝑋 ) ( .r𝑊 ) 𝑋 ) ) )
274 eqid ( 1r ‘ ( 𝐽 mPoly 𝑅 ) ) = ( 1r ‘ ( 𝐽 mPoly 𝑅 ) )
275 41 46 274 esplyfval0 ( 𝜑 → ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) = ( 1r ‘ ( 𝐽 mPoly 𝑅 ) ) )
276 275 fveq2d ( 𝜑 → ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) = ( ( 𝐽 eval 𝑅 ) ‘ ( 1r ‘ ( 𝐽 mPoly 𝑅 ) ) ) )
277 eqid ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) = ( algSc ‘ ( 𝐽 mPoly 𝑅 ) )
278 eqid ( 1r𝑅 ) = ( 1r𝑅 )
279 162 277 278 274 41 46 mplascl1 ( 𝜑 → ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 1r𝑅 ) ) = ( 1r ‘ ( 𝐽 mPoly 𝑅 ) ) )
280 279 fveq2d ( 𝜑 → ( ( 𝐽 eval 𝑅 ) ‘ ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 1r𝑅 ) ) ) = ( ( 𝐽 eval 𝑅 ) ‘ ( 1r ‘ ( 𝐽 mPoly 𝑅 ) ) ) )
281 276 280 eqtr4d ( 𝜑 → ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) = ( ( 𝐽 eval 𝑅 ) ‘ ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 1r𝑅 ) ) ) )
282 281 fveq1d ( 𝜑 → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) = ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 1r𝑅 ) ) ) ‘ ( 𝑍𝐽 ) ) )
283 161 162 2 277 41 35 246 142 evlscaval ( 𝜑 → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 1r𝑅 ) ) ) ‘ ( 𝑍𝐽 ) ) = ( 1r𝑅 ) )
284 282 283 eqtrd ( 𝜑 → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) = ( 1r𝑅 ) )
285 284 oveq2d ( 𝜑 → ( ( 0 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) ) = ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) )
286 32 81 34 mulgnn0p1 ( ( 𝑀 ∈ Mnd ∧ ( ♯ ‘ 𝐽 ) ∈ ℕ0𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝐽 ) + 1 ) ( .g𝑀 ) 𝑋 ) = ( ( ( ♯ ‘ 𝐽 ) ( .g𝑀 ) 𝑋 ) ( .r𝑊 ) 𝑋 ) )
287 117 100 48 286 syl3anc ( 𝜑 → ( ( ( ♯ ‘ 𝐽 ) + 1 ) ( .g𝑀 ) 𝑋 ) = ( ( ( ♯ ‘ 𝐽 ) ( .g𝑀 ) 𝑋 ) ( .r𝑊 ) 𝑋 ) )
288 hashdifsn ( ( 𝐼 ∈ Fin ∧ 𝑌𝐼 ) → ( ♯ ‘ ( 𝐼 ∖ { 𝑌 } ) ) = ( ( ♯ ‘ 𝐼 ) − 1 ) )
289 14 19 288 syl2anc ( 𝜑 → ( ♯ ‘ ( 𝐼 ∖ { 𝑌 } ) ) = ( ( ♯ ‘ 𝐼 ) − 1 ) )
290 20 fveq2i ( ♯ ‘ 𝐽 ) = ( ♯ ‘ ( 𝐼 ∖ { 𝑌 } ) )
291 13 oveq1i ( 𝐻 − 1 ) = ( ( ♯ ‘ 𝐼 ) − 1 )
292 289 290 291 3eqtr4g ( 𝜑 → ( ♯ ‘ 𝐽 ) = ( 𝐻 − 1 ) )
293 292 oveq1d ( 𝜑 → ( ( ♯ ‘ 𝐽 ) + 1 ) = ( ( 𝐻 − 1 ) + 1 ) )
294 250 nn0cnd ( 𝜑𝐻 ∈ ℂ )
295 1cnd ( 𝜑 → 1 ∈ ℂ )
296 294 295 npcand ( 𝜑 → ( ( 𝐻 − 1 ) + 1 ) = 𝐻 )
297 293 296 eqtr2d ( 𝜑𝐻 = ( ( ♯ ‘ 𝐽 ) + 1 ) )
298 297 oveq1d ( 𝜑 → ( 𝐻 ( .g𝑀 ) 𝑋 ) = ( ( ( ♯ ‘ 𝐽 ) + 1 ) ( .g𝑀 ) 𝑋 ) )
299 270 oveq1d ( 𝜑 → ( ( ( ♯ ‘ 𝐽 ) − 0 ) ( .g𝑀 ) 𝑋 ) = ( ( ♯ ‘ 𝐽 ) ( .g𝑀 ) 𝑋 ) )
300 299 oveq1d ( 𝜑 → ( ( ( ( ♯ ‘ 𝐽 ) − 0 ) ( .g𝑀 ) 𝑋 ) ( .r𝑊 ) 𝑋 ) = ( ( ( ♯ ‘ 𝐽 ) ( .g𝑀 ) 𝑋 ) ( .r𝑊 ) 𝑋 ) )
301 287 298 300 3eqtr4rd ( 𝜑 → ( ( ( ( ♯ ‘ 𝐽 ) − 0 ) ( .g𝑀 ) 𝑋 ) ( .r𝑊 ) 𝑋 ) = ( 𝐻 ( .g𝑀 ) 𝑋 ) )
302 285 301 oveq12d ( 𝜑 → ( ( ( 0 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ( ♯ ‘ 𝐽 ) − 0 ) ( .g𝑀 ) 𝑋 ) ( .r𝑊 ) 𝑋 ) ) = ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) )
303 273 302 eqtr2d ( 𝜑 → ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) = ( ( ( ( 0 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 0 ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) 𝑋 ) )
304 62 fveq2d ( 𝜑 → ( .r𝑅 ) = ( .r ‘ ( Scalar ‘ 𝑊 ) ) )
305 9 304 eqtrid ( 𝜑· = ( .r ‘ ( Scalar ‘ 𝑊 ) ) )
306 305 oveqd ( 𝜑 → ( ( 𝑍𝑌 ) · ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ) = ( ( 𝑍𝑌 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ) )
307 306 oveq1d ( 𝜑 → ( ( ( 𝑍𝑌 ) · ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( 𝑍𝑌 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) )
308 16 19 ffvelcdmd ( 𝜑 → ( 𝑍𝑌 ) ∈ 𝐵 )
309 150 12 242 100 158 mulgnn0cld ( 𝜑 → ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) ∈ 𝐵 )
310 166 41 46 100 163 esplympl ( 𝜑 → ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
311 161 162 163 2 41 35 310 143 evlcl ( 𝜑 → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ∈ 𝐵 )
312 2 9 35 308 309 311 crng12d ( 𝜑 → ( ( 𝑍𝑌 ) · ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ) = ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ) )
313 297 oveq1d ( 𝜑 → ( 𝐻 ( 𝑁1 ) ) = ( ( ( ♯ ‘ 𝐽 ) + 1 ) ( 𝑁1 ) ) )
314 8 7 12 46 100 ringm1expp1 ( 𝜑 → ( ( ( ♯ ‘ 𝐽 ) + 1 ) ( 𝑁1 ) ) = ( 𝑁 ‘ ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) ) )
315 313 314 eqtrd ( 𝜑 → ( 𝐻 ( 𝑁1 ) ) = ( 𝑁 ‘ ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) ) )
316 315 fveq2d ( 𝜑 → ( 𝑁 ‘ ( 𝐻 ( 𝑁1 ) ) ) = ( 𝑁 ‘ ( 𝑁 ‘ ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) ) ) )
317 2 7 156 309 grpinvinvd ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) ) ) = ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) )
318 316 317 eqtrd ( 𝜑 → ( 𝑁 ‘ ( 𝐻 ( 𝑁1 ) ) ) = ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) )
319 eqid ( +g𝑅 ) = ( +g𝑅 )
320 eqid ( 𝐽 eSymPoly 𝑅 ) = ( 𝐽 eSymPoly 𝑅 )
321 eqid ( ♯ ‘ 𝐽 ) = ( ♯ ‘ 𝐽 )
322 2 319 9 5 161 6 320 13 321 20 14 35 19 16 esplyfvn ( 𝜑 → ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) = ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) )
323 318 322 oveq12d ( 𝜑 → ( ( 𝑁 ‘ ( 𝐻 ( 𝑁1 ) ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) = ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ) )
324 312 323 eqtr4d ( 𝜑 → ( ( 𝑍𝑌 ) · ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ) = ( ( 𝑁 ‘ ( 𝐻 ( 𝑁1 ) ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) )
325 2 9 7 46 253 261 ringmneg1 ( 𝜑 → ( ( 𝑁 ‘ ( 𝐻 ( 𝑁1 ) ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) = ( 𝑁 ‘ ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ) )
326 62 fveq2d ( 𝜑 → ( invg𝑅 ) = ( invg ‘ ( Scalar ‘ 𝑊 ) ) )
327 7 326 eqtrid ( 𝜑𝑁 = ( invg ‘ ( Scalar ‘ 𝑊 ) ) )
328 327 fveq1d ( 𝜑 → ( 𝑁 ‘ ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ) = ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ) )
329 324 325 328 3eqtrd ( 𝜑 → ( ( 𝑍𝑌 ) · ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ) = ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ) )
330 172 subidd ( 𝜑 → ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) = 0 )
331 330 oveq1d ( 𝜑 → ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) = ( 0 ( .g𝑀 ) 𝑋 ) )
332 329 331 oveq12d ( 𝜑 → ( ( ( 𝑍𝑌 ) · ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) )
333 2 9 46 309 311 ringcld ( 𝜑 → ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ 𝐵 )
334 333 64 eleqtrd ( 𝜑 → ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
335 330 244 eqeltrd ( 𝜑 → ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ∈ ℕ0 )
336 32 81 117 335 48 mulgnn0cld ( 𝜑 → ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
337 eqid ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
338 31 50 80 51 337 lmodvsass ( ( 𝑊 ∈ LMod ∧ ( ( 𝑍𝑌 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) ) ) → ( ( ( 𝑍𝑌 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) = ( ( 𝑍𝑌 ) ( ·𝑠𝑊 ) ( ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) ) )
339 102 73 334 336 338 syl13anc ( 𝜑 → ( ( ( 𝑍𝑌 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) = ( ( 𝑍𝑌 ) ( ·𝑠𝑊 ) ( ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) ) )
340 307 332 339 3eqtr3d ( 𝜑 → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) = ( ( 𝑍𝑌 ) ( ·𝑠𝑊 ) ( ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) ) )
341 eqid ( invg ‘ ( Scalar ‘ 𝑊 ) ) = ( invg ‘ ( Scalar ‘ 𝑊 ) )
342 262 64 eleqtrd ( 𝜑 → ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
343 31 50 80 241 51 341 102 263 342 lmodvsneg ( 𝜑 → ( ( invg𝑊 ) ‘ ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) = ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) )
344 1 31 2 80 46 333 336 ply1vscl ( 𝜑 → ( ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) )
345 11 50 51 31 33 80 asclmul2 ( ( 𝑊 ∈ AssAlg ∧ ( 𝑍𝑌 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) ) → ( ( ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) = ( ( 𝑍𝑌 ) ( ·𝑠𝑊 ) ( ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) ) )
346 53 73 344 345 syl3anc ( 𝜑 → ( ( ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) = ( ( 𝑍𝑌 ) ( ·𝑠𝑊 ) ( ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) ) )
347 340 343 346 3eqtr4d ( 𝜑 → ( ( invg𝑊 ) ‘ ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) = ( ( ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) )
348 303 347 oveq12d ( 𝜑 → ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( ( invg𝑊 ) ‘ ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) ) = ( ( ( ( ( 0 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 0 ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) 𝑋 ) ( ( ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) ) )
349 265 348 eqtr3d ( 𝜑 → ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) = ( ( ( ( ( 0 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 0 ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) 𝑋 ) ( ( ( ( ( ♯ ‘ 𝐽 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ♯ ‘ 𝐽 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( ♯ ‘ 𝐽 ) ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) ) )
350 46 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑅 ∈ Ring )
351 350 151 syl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
352 fzossfz ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐽 ) )
353 simpr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) )
354 352 353 sselid ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
355 110 354 sselid ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑘 ∈ ℕ0 )
356 peano2nn0 ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
357 355 356 syl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑘 + 1 ) ∈ ℕ0 )
358 158 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑁1 ) ∈ 𝐵 )
359 150 12 351 357 358 mulgnn0cld ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑘 + 1 ) ( 𝑁1 ) ) ∈ 𝐵 )
360 41 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝐽 ∈ Fin )
361 35 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑅 ∈ CRing )
362 166 360 350 357 163 esplympl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
363 143 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑍𝐽 ) ∈ ( 𝐵m 𝐽 ) )
364 161 162 163 2 360 361 362 363 evlcl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ∈ 𝐵 )
365 16 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑍 : 𝐼𝐵 )
366 19 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑌𝐼 )
367 365 366 ffvelcdmd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑍𝑌 ) ∈ 𝐵 )
368 166 360 350 355 163 esplympl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
369 161 162 163 2 360 361 368 363 evlcl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ∈ 𝐵 )
370 2 9 350 367 369 ringcld ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ 𝐵 )
371 2 319 9 350 359 364 370 ringdid ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ( +g𝑅 ) ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) ) = ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( +g𝑅 ) ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) ) )
372 14 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝐼 ∈ Fin )
373 6 fveq1i ( 𝐸 ‘ ( 𝑘 + 1 ) ) = ( ( 𝐼 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) )
374 9 372 361 366 20 320 354 166 373 2 5 161 319 365 esplyindfv ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) = ( ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( +g𝑅 ) ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) )
375 46 ringabld ( 𝜑𝑅 ∈ Abel )
376 375 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑅 ∈ Abel )
377 2 319 376 370 364 ablcomd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( +g𝑅 ) ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) = ( ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ( +g𝑅 ) ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) )
378 374 377 eqtrd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) = ( ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ( +g𝑅 ) ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) )
379 378 oveq2d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) ) = ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ( +g𝑅 ) ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) ) )
380 eqid ( -g𝑅 ) = ( -g𝑅 )
381 156 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑅 ∈ Grp )
382 2 9 350 359 364 ringcld ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ 𝐵 )
383 2 9 350 359 370 ringcld ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) ∈ 𝐵 )
384 2 319 380 7 381 382 383 grpsubinv ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( -g𝑅 ) ( 𝑁 ‘ ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) ) ) = ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( +g𝑅 ) ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) ) )
385 371 379 384 3eqtr4d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) ) = ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( -g𝑅 ) ( 𝑁 ‘ ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) ) ) )
386 62 fveq2d ( 𝜑 → ( -g𝑅 ) = ( -g ‘ ( Scalar ‘ 𝑊 ) ) )
387 386 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( -g𝑅 ) = ( -g ‘ ( Scalar ‘ 𝑊 ) ) )
388 eqidd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) = ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) )
389 242 adantr ( ( 𝜑𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
390 simpr ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
391 158 adantr ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝑁1 ) ∈ 𝐵 )
392 150 12 389 390 391 mulgnn0cld ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝑘 ( 𝑁1 ) ) ∈ 𝐵 )
393 355 392 syldan ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑘 ( 𝑁1 ) ) ∈ 𝐵 )
394 2 9 350 393 369 367 ringassd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) = ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) · ( 𝑍𝑌 ) ) ) )
395 8 7 12 350 355 ringm1expp1 ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑘 + 1 ) ( 𝑁1 ) ) = ( 𝑁 ‘ ( 𝑘 ( 𝑁1 ) ) ) )
396 395 fveq2d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑁 ‘ ( ( 𝑘 + 1 ) ( 𝑁1 ) ) ) = ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑘 ( 𝑁1 ) ) ) ) )
397 2 7 381 393 grpinvinvd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑘 ( 𝑁1 ) ) ) ) = ( 𝑘 ( 𝑁1 ) ) )
398 396 397 eqtrd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑁 ‘ ( ( 𝑘 + 1 ) ( 𝑁1 ) ) ) = ( 𝑘 ( 𝑁1 ) ) )
399 2 9 361 367 369 crngcomd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) = ( ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) · ( 𝑍𝑌 ) ) )
400 398 399 oveq12d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑁 ‘ ( ( 𝑘 + 1 ) ( 𝑁1 ) ) ) · ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) = ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) · ( 𝑍𝑌 ) ) ) )
401 2 9 7 350 359 370 ringmneg1 ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑁 ‘ ( ( 𝑘 + 1 ) ( 𝑁1 ) ) ) · ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) = ( 𝑁 ‘ ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) ) )
402 394 400 401 3eqtr2rd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑁 ‘ ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) ) = ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) )
403 387 388 402 oveq123d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( -g𝑅 ) ( 𝑁 ‘ ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑍𝑌 ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) ) ) = ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) ) )
404 385 403 eqtrd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) ) = ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) ) )
405 404 oveq1d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) )
406 eqid ( -g ‘ ( Scalar ‘ 𝑊 ) ) = ( -g ‘ ( Scalar ‘ 𝑊 ) )
407 350 101 syl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑊 ∈ LMod )
408 64 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝐵 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
409 382 408 eleqtrd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
410 2 9 350 393 369 ringcld ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ 𝐵 )
411 2 9 350 410 367 ringcld ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) ∈ 𝐵 )
412 411 408 eleqtrd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
413 117 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑀 ∈ Mnd )
414 fz0ssnn0 ( 0 ... 𝐻 ) ⊆ ℕ0
415 fzossfz ( 0 ..^ 𝐻 ) ⊆ ( 0 ... 𝐻 )
416 fzssp1 ( 1 ... ( ♯ ‘ 𝐽 ) ) ⊆ ( 1 ... ( ( ♯ ‘ 𝐽 ) + 1 ) )
417 297 oveq2d ( 𝜑 → ( 1 ... 𝐻 ) = ( 1 ... ( ( ♯ ‘ 𝐽 ) + 1 ) ) )
418 416 417 sseqtrrid ( 𝜑 → ( 1 ... ( ♯ ‘ 𝐽 ) ) ⊆ ( 1 ... 𝐻 ) )
419 418 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 1 ... ( ♯ ‘ 𝐽 ) ) ⊆ ( 1 ... 𝐻 ) )
420 360 99 syl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ♯ ‘ 𝐽 ) ∈ ℕ0 )
421 fz0add1fz1 ( ( ( ♯ ‘ 𝐽 ) ∈ ℕ0𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) )
422 420 353 421 syl2anc ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) )
423 419 422 sseldd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐻 ) )
424 ubmelfzo ( ( 𝑘 + 1 ) ∈ ( 1 ... 𝐻 ) → ( 𝐻 − ( 𝑘 + 1 ) ) ∈ ( 0 ..^ 𝐻 ) )
425 423 424 syl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝐻 − ( 𝑘 + 1 ) ) ∈ ( 0 ..^ 𝐻 ) )
426 415 425 sselid ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝐻 − ( 𝑘 + 1 ) ) ∈ ( 0 ... 𝐻 ) )
427 414 426 sselid ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝐻 − ( 𝑘 + 1 ) ) ∈ ℕ0 )
428 350 47 syl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
429 32 81 413 427 428 mulgnn0cld ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
430 31 80 50 51 3 406 407 409 412 429 lmodsubdir ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) ( ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) ) )
431 297 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝐻 = ( ( ♯ ‘ 𝐽 ) + 1 ) )
432 431 oveq1d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝐻 − ( 𝑘 + 1 ) ) = ( ( ( ♯ ‘ 𝐽 ) + 1 ) − ( 𝑘 + 1 ) ) )
433 172 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ♯ ‘ 𝐽 ) ∈ ℂ )
434 1cnd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 1 ∈ ℂ )
435 357 nn0cnd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑘 + 1 ) ∈ ℂ )
436 433 434 435 addsubd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ♯ ‘ 𝐽 ) + 1 ) − ( 𝑘 + 1 ) ) = ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) + 1 ) )
437 432 436 eqtrd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝐻 − ( 𝑘 + 1 ) ) = ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) + 1 ) )
438 437 oveq1d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) = ( ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) + 1 ) ( .g𝑀 ) 𝑋 ) )
439 fzofzp1 ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) → ( 𝑘 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
440 439 adantl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑘 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
441 fznn0sub2 ( ( 𝑘 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) → ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
442 440 441 syl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
443 110 442 sselid ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ∈ ℕ0 )
444 32 81 34 mulgnn0p1 ( ( 𝑀 ∈ Mnd ∧ ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ∈ ℕ0𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) + 1 ) ( .g𝑀 ) 𝑋 ) = ( ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ( .r𝑊 ) 𝑋 ) )
445 413 443 428 444 syl3anc ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) + 1 ) ( .g𝑀 ) 𝑋 ) = ( ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ( .r𝑊 ) 𝑋 ) )
446 438 445 eqtrd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) = ( ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ( .r𝑊 ) 𝑋 ) )
447 446 oveq2d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ( .r𝑊 ) 𝑋 ) ) )
448 361 52 syl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑊 ∈ AssAlg )
449 32 81 413 443 428 mulgnn0cld ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
450 31 50 51 80 33 448 409 449 428 assaassd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) 𝑋 ) = ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ( .r𝑊 ) 𝑋 ) ) )
451 447 450 eqtr4d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) 𝑋 ) )
452 73 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝑍𝑌 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
453 410 408 eleqtrd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
454 fznn0sub2 ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
455 354 454 syl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
456 110 455 sselid ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ∈ ℕ0 )
457 32 81 413 456 428 mulgnn0cld ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
458 31 50 80 51 337 lmodvsass ( ( 𝑊 ∈ LMod ∧ ( ( 𝑍𝑌 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) ) ) → ( ( ( 𝑍𝑌 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) = ( ( 𝑍𝑌 ) ( ·𝑠𝑊 ) ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) )
459 407 452 453 457 458 syl13anc ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑍𝑌 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) = ( ( 𝑍𝑌 ) ( ·𝑠𝑊 ) ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) )
460 2 9 361 410 367 crngcomd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) = ( ( 𝑍𝑌 ) · ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) )
461 305 oveqd ( 𝜑 → ( ( 𝑍𝑌 ) · ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) = ( ( 𝑍𝑌 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) )
462 461 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑍𝑌 ) · ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) = ( ( 𝑍𝑌 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) )
463 460 462 eqtrd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) = ( ( 𝑍𝑌 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) )
464 292 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ♯ ‘ 𝐽 ) = ( 𝐻 − 1 ) )
465 464 oveq1d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑘 ) = ( ( 𝐻 − 1 ) − 𝑘 ) )
466 294 adantr ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝐻 ∈ ℂ )
467 355 nn0cnd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → 𝑘 ∈ ℂ )
468 466 467 434 sub32d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐻𝑘 ) − 1 ) = ( ( 𝐻 − 1 ) − 𝑘 ) )
469 466 467 434 subsub4d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐻𝑘 ) − 1 ) = ( 𝐻 − ( 𝑘 + 1 ) ) )
470 465 468 469 3eqtr2rd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( 𝐻 − ( 𝑘 + 1 ) ) = ( ( ♯ ‘ 𝐽 ) − 𝑘 ) )
471 470 oveq1d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) = ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) )
472 463 471 oveq12d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( 𝑍𝑌 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) )
473 1 31 2 80 350 410 457 ply1vscl ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) )
474 11 50 51 31 33 80 asclmul2 ( ( 𝑊 ∈ AssAlg ∧ ( 𝑍𝑌 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) ) → ( ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) = ( ( 𝑍𝑌 ) ( ·𝑠𝑊 ) ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) )
475 448 452 473 474 syl3anc ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) = ( ( 𝑍𝑌 ) ( ·𝑠𝑊 ) ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) )
476 459 472 475 3eqtr4d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) )
477 451 476 oveq12d ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) ( ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) · ( 𝑍𝑌 ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) ) = ( ( ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) 𝑋 ) ( ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) ) )
478 405 430 477 3eqtrd ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝑘 + 1 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) 𝑋 ) ( ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ( .r𝑊 ) ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) ) )
479 31 193 3 33 43 48 74 100 212 219 226 233 240 349 478 gsummulsubdishift2s ( 𝜑 → ( ( 𝑊 Σg ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) ) ( .r𝑊 ) ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) ) = ( ( 𝑊 Σg ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) ) )
480 46 adantr ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑅 ∈ Ring )
481 480 151 syl ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
482 110 a1i ( 𝜑 → ( 0 ... ( ♯ ‘ 𝐽 ) ) ⊆ ℕ0 )
483 482 sselda ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑘 ∈ ℕ0 )
484 158 adantr ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑁1 ) ∈ 𝐵 )
485 150 12 481 483 484 mulgnn0cld ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑘 ( 𝑁1 ) ) ∈ 𝐵 )
486 41 adantr ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝐽 ∈ Fin )
487 35 adantr ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑅 ∈ CRing )
488 166 486 480 483 163 esplympl ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
489 143 adantr ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑍𝐽 ) ∈ ( 𝐵m 𝐽 ) )
490 161 162 163 2 486 487 488 489 evlcl ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ∈ 𝐵 )
491 2 9 480 485 490 ringcld ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ∈ 𝐵 )
492 117 adantr ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑀 ∈ Mnd )
493 454 adantl ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
494 110 493 sselid ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ∈ ℕ0 )
495 48 adantr ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
496 32 81 492 494 495 mulgnn0cld ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
497 1 31 2 80 480 491 496 ply1vscl ( ( 𝜑𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) )
498 oveq1 ( 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) → ( 𝑘 ( 𝑁1 ) ) = ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) )
499 2fveq3 ( 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) → ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) = ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) )
500 499 fveq1d ( 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) → ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) = ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) )
501 498 500 oveq12d ( 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) → ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) = ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) )
502 501 adantl ( ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) → ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) = ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) )
503 simpr ( ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) → 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) )
504 503 oveq2d ( ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑘 ) = ( ( ♯ ‘ 𝐽 ) − ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) )
505 172 ad2antrr ( ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) → ( ♯ ‘ 𝐽 ) ∈ ℂ )
506 112 adantr ( ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) → 𝑙 ∈ ℕ0 )
507 506 nn0cnd ( ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) → 𝑙 ∈ ℂ )
508 505 507 nncand ( ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) → ( ( ♯ ‘ 𝐽 ) − ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) = 𝑙 )
509 504 508 eqtrd ( ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) → ( ( ♯ ‘ 𝐽 ) − 𝑘 ) = 𝑙 )
510 509 oveq1d ( ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) → ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) = ( 𝑙 ( .g𝑀 ) 𝑋 ) )
511 502 510 oveq12d ( ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑘 = ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) → ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) )
512 31 98 100 497 511 gsummptrev ( 𝜑 → ( 𝑊 Σg ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) )
513 512 oveq1d ( 𝜑 → ( ( 𝑊 Σg ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( ( ( ♯ ‘ 𝐽 ) − 𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) ) ( .r𝑊 ) ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) ) = ( ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) ( .r𝑊 ) ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) ) )
514 46 adantr ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑅 ∈ Ring )
515 514 151 syl ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
516 fz1ssfz0 ( 1 ... ( ♯ ‘ 𝐽 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐽 ) )
517 516 110 sstri ( 1 ... ( ♯ ‘ 𝐽 ) ) ⊆ ℕ0
518 517 a1i ( 𝜑 → ( 1 ... ( ♯ ‘ 𝐽 ) ) ⊆ ℕ0 )
519 518 sselda ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑙 ∈ ℕ0 )
520 158 adantr ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑁1 ) ∈ 𝐵 )
521 150 12 515 519 520 mulgnn0cld ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑙 ( 𝑁1 ) ) ∈ 𝐵 )
522 14 adantr ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → 𝐼 ∈ Fin )
523 35 adantr ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑅 ∈ CRing )
524 6 fveq1i ( 𝐸𝑙 ) = ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝑙 )
525 257 522 514 519 255 esplympl ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝑙 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
526 524 525 eqeltrid ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝐸𝑙 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
527 260 adantr ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑍 ∈ ( 𝐵m 𝐼 ) )
528 5 254 255 2 522 523 526 527 evlcl ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ∈ 𝐵 )
529 2 9 514 521 528 ringcld ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ∈ 𝐵 )
530 117 adantr ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑀 ∈ Mnd )
531 fzssp1 ( 0 ... ( ♯ ‘ 𝐽 ) ) ⊆ ( 0 ... ( ( ♯ ‘ 𝐽 ) + 1 ) )
532 297 oveq2d ( 𝜑 → ( 0 ... 𝐻 ) = ( 0 ... ( ( ♯ ‘ 𝐽 ) + 1 ) ) )
533 531 532 sseqtrrid ( 𝜑 → ( 0 ... ( ♯ ‘ 𝐽 ) ) ⊆ ( 0 ... 𝐻 ) )
534 516 533 sstrid ( 𝜑 → ( 1 ... ( ♯ ‘ 𝐽 ) ) ⊆ ( 0 ... 𝐻 ) )
535 534 sselda ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑙 ∈ ( 0 ... 𝐻 ) )
536 fznn0sub2 ( 𝑙 ∈ ( 0 ... 𝐻 ) → ( 𝐻𝑙 ) ∈ ( 0 ... 𝐻 ) )
537 535 536 syl ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝐻𝑙 ) ∈ ( 0 ... 𝐻 ) )
538 414 537 sselid ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝐻𝑙 ) ∈ ℕ0 )
539 514 47 syl ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
540 32 81 530 538 539 mulgnn0cld ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
541 1 31 2 80 514 529 540 ply1vscl ( ( 𝜑𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) )
542 oveq1 ( 𝑙 = ( 𝑘 + 1 ) → ( 𝑙 ( 𝑁1 ) ) = ( ( 𝑘 + 1 ) ( 𝑁1 ) ) )
543 2fveq3 ( 𝑙 = ( 𝑘 + 1 ) → ( 𝑄 ‘ ( 𝐸𝑙 ) ) = ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) )
544 543 fveq1d ( 𝑙 = ( 𝑘 + 1 ) → ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) )
545 542 544 oveq12d ( 𝑙 = ( 𝑘 + 1 ) → ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) = ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) ) )
546 oveq2 ( 𝑙 = ( 𝑘 + 1 ) → ( 𝐻𝑙 ) = ( 𝐻 − ( 𝑘 + 1 ) ) )
547 546 oveq1d ( 𝑙 = ( 𝑘 + 1 ) → ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) = ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) )
548 545 547 oveq12d ( 𝑙 = ( 𝑘 + 1 ) → ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) )
549 548 adantl ( ( ( 𝜑𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ) ∧ 𝑙 = ( 𝑘 + 1 ) ) → ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) )
550 31 98 100 541 549 gsummptp1 ( 𝜑 → ( 𝑊 Σg ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) )
551 550 oveq1d ( 𝜑 → ( ( 𝑊 Σg ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) ) = ( ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) ) )
552 oveq1 ( 𝑘 = 𝑙 → ( 𝑘 ( 𝑁1 ) ) = ( 𝑙 ( 𝑁1 ) ) )
553 2fveq3 ( 𝑘 = 𝑙 → ( 𝑄 ‘ ( 𝐸𝑘 ) ) = ( 𝑄 ‘ ( 𝐸𝑙 ) ) )
554 553 fveq1d ( 𝑘 = 𝑙 → ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) )
555 552 554 oveq12d ( 𝑘 = 𝑙 → ( ( 𝑘 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) ) = ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) )
556 oveq2 ( 𝑘 = 𝑙 → ( 𝐻𝑘 ) = ( 𝐻𝑙 ) )
557 556 oveq1d ( 𝑘 = 𝑙 → ( ( 𝐻𝑘 ) ( .g𝑀 ) 𝑋 ) = ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) )
558 555 557 oveq12d ( 𝑘 = 𝑙 → ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑘 ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) )
559 558 cbvmptv ( 𝑘 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) = ( 𝑙 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) )
560 559 a1i ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) = ( 𝑙 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) )
561 560 oveq2d ( 𝜑 → ( 𝑊 Σg ( 𝑘 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) )
562 nn0uz 0 = ( ℤ ‘ 0 )
563 250 562 eleqtrdi ( 𝜑𝐻 ∈ ( ℤ ‘ 0 ) )
564 46 adantr ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → 𝑅 ∈ Ring )
565 564 151 syl ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
566 414 a1i ( 𝜑 → ( 0 ... 𝐻 ) ⊆ ℕ0 )
567 566 sselda ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → 𝑙 ∈ ℕ0 )
568 158 adantr ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( 𝑁1 ) ∈ 𝐵 )
569 150 12 565 567 568 mulgnn0cld ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( 𝑙 ( 𝑁1 ) ) ∈ 𝐵 )
570 14 adantr ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → 𝐼 ∈ Fin )
571 35 adantr ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → 𝑅 ∈ CRing )
572 257 570 564 567 255 esplympl ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝑙 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
573 524 572 eqeltrid ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( 𝐸𝑙 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
574 260 adantr ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → 𝑍 ∈ ( 𝐵m 𝐼 ) )
575 5 254 255 2 570 571 573 574 evlcl ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ∈ 𝐵 )
576 2 9 564 569 575 ringcld ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ∈ 𝐵 )
577 117 adantr ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → 𝑀 ∈ Mnd )
578 fznn0sub ( 𝑙 ∈ ( 0 ... 𝐻 ) → ( 𝐻𝑙 ) ∈ ℕ0 )
579 578 adantl ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( 𝐻𝑙 ) ∈ ℕ0 )
580 564 47 syl ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
581 32 81 577 579 580 mulgnn0cld ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
582 1 31 2 80 564 576 581 ply1vscl ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) )
583 oveq1 ( 𝑙 = 𝐻 → ( 𝑙 ( 𝑁1 ) ) = ( 𝐻 ( 𝑁1 ) ) )
584 2fveq3 ( 𝑙 = 𝐻 → ( 𝑄 ‘ ( 𝐸𝑙 ) ) = ( 𝑄 ‘ ( 𝐸𝐻 ) ) )
585 584 fveq1d ( 𝑙 = 𝐻 → ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) )
586 583 585 oveq12d ( 𝑙 = 𝐻 → ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) = ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) )
587 586 adantl ( ( 𝜑𝑙 = 𝐻 ) → ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) = ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) )
588 oveq2 ( 𝑙 = 𝐻 → ( 𝐻𝑙 ) = ( 𝐻𝐻 ) )
589 294 subidd ( 𝜑 → ( 𝐻𝐻 ) = 0 )
590 588 589 sylan9eqr ( ( 𝜑𝑙 = 𝐻 ) → ( 𝐻𝑙 ) = 0 )
591 590 oveq1d ( ( 𝜑𝑙 = 𝐻 ) → ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) = ( 0 ( .g𝑀 ) 𝑋 ) )
592 587 591 oveq12d ( ( 𝜑𝑙 = 𝐻 ) → ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) )
593 31 193 98 563 582 592 gsummptfzsplitra ( 𝜑 → ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) = ( ( 𝑊 Σg ( 𝑙 ∈ ( 0 ..^ 𝐻 ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) )
594 100 nn0zd ( 𝜑 → ( ♯ ‘ 𝐽 ) ∈ ℤ )
595 fzval3 ( ( ♯ ‘ 𝐽 ) ∈ ℤ → ( 0 ... ( ♯ ‘ 𝐽 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐽 ) + 1 ) ) )
596 594 595 syl ( 𝜑 → ( 0 ... ( ♯ ‘ 𝐽 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐽 ) + 1 ) ) )
597 297 oveq2d ( 𝜑 → ( 0 ..^ 𝐻 ) = ( 0 ..^ ( ( ♯ ‘ 𝐽 ) + 1 ) ) )
598 596 597 eqtr4d ( 𝜑 → ( 0 ... ( ♯ ‘ 𝐽 ) ) = ( 0 ..^ 𝐻 ) )
599 598 mpteq1d ( 𝜑 → ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) = ( 𝑙 ∈ ( 0 ..^ 𝐻 ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) )
600 599 oveq2d ( 𝜑 → ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 0 ..^ 𝐻 ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) )
601 100 562 eleqtrdi ( 𝜑 → ( ♯ ‘ 𝐽 ) ∈ ( ℤ ‘ 0 ) )
602 150 12 152 112 159 mulgnn0cld ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝑙 ( 𝑁1 ) ) ∈ 𝐵 )
603 14 adantr ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝐼 ∈ Fin )
604 257 603 119 112 255 esplympl ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝑙 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
605 524 604 eqeltrid ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝐸𝑙 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
606 260 adantr ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑍 ∈ ( 𝐵m 𝐼 ) )
607 5 254 255 2 603 165 605 606 evlcl ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ∈ 𝐵 )
608 2 9 119 602 607 ringcld ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ∈ 𝐵 )
609 533 sselda ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → 𝑙 ∈ ( 0 ... 𝐻 ) )
610 609 536 syl ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝐻𝑙 ) ∈ ( 0 ... 𝐻 ) )
611 414 610 sselid ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( 𝐻𝑙 ) ∈ ℕ0 )
612 32 81 118 611 120 mulgnn0cld ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
613 1 31 2 80 119 608 612 ply1vscl ( ( 𝜑𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) → ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) )
614 oveq1 ( 𝑙 = 0 → ( 𝑙 ( 𝑁1 ) ) = ( 0 ( 𝑁1 ) ) )
615 614 adantl ( ( 𝜑𝑙 = 0 ) → ( 𝑙 ( 𝑁1 ) ) = ( 0 ( 𝑁1 ) ) )
616 2fveq3 ( 𝑙 = 0 → ( 𝑄 ‘ ( 𝐸𝑙 ) ) = ( 𝑄 ‘ ( 𝐸 ‘ 0 ) ) )
617 616 fveq1d ( 𝑙 = 0 → ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( 𝐸 ‘ 0 ) ) ‘ 𝑍 ) )
618 617 adantl ( ( 𝜑𝑙 = 0 ) → ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( 𝐸 ‘ 0 ) ) ‘ 𝑍 ) )
619 eqid ( 1r ‘ ( 𝐼 mPoly 𝑅 ) ) = ( 1r ‘ ( 𝐼 mPoly 𝑅 ) )
620 14 46 619 esplyfval0 ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 0 ) = ( 1r ‘ ( 𝐼 mPoly 𝑅 ) ) )
621 6 fveq1i ( 𝐸 ‘ 0 ) = ( ( 𝐼 eSymPoly 𝑅 ) ‘ 0 )
622 621 a1i ( 𝜑 → ( 𝐸 ‘ 0 ) = ( ( 𝐼 eSymPoly 𝑅 ) ‘ 0 ) )
623 eqid ( algSc ‘ ( 𝐼 mPoly 𝑅 ) ) = ( algSc ‘ ( 𝐼 mPoly 𝑅 ) )
624 254 623 278 619 14 46 mplascl1 ( 𝜑 → ( ( algSc ‘ ( 𝐼 mPoly 𝑅 ) ) ‘ ( 1r𝑅 ) ) = ( 1r ‘ ( 𝐼 mPoly 𝑅 ) ) )
625 620 622 624 3eqtr4d ( 𝜑 → ( 𝐸 ‘ 0 ) = ( ( algSc ‘ ( 𝐼 mPoly 𝑅 ) ) ‘ ( 1r𝑅 ) ) )
626 625 fveq2d ( 𝜑 → ( 𝑄 ‘ ( 𝐸 ‘ 0 ) ) = ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑅 ) ) ‘ ( 1r𝑅 ) ) ) )
627 626 fveq1d ( 𝜑 → ( ( 𝑄 ‘ ( 𝐸 ‘ 0 ) ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑅 ) ) ‘ ( 1r𝑅 ) ) ) ‘ 𝑍 ) )
628 627 adantr ( ( 𝜑𝑙 = 0 ) → ( ( 𝑄 ‘ ( 𝐸 ‘ 0 ) ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑅 ) ) ‘ ( 1r𝑅 ) ) ) ‘ 𝑍 ) )
629 5 254 2 623 14 35 246 16 evlscaval ( 𝜑 → ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑅 ) ) ‘ ( 1r𝑅 ) ) ) ‘ 𝑍 ) = ( 1r𝑅 ) )
630 629 adantr ( ( 𝜑𝑙 = 0 ) → ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑅 ) ) ‘ ( 1r𝑅 ) ) ) ‘ 𝑍 ) = ( 1r𝑅 ) )
631 618 628 630 3eqtrd ( ( 𝜑𝑙 = 0 ) → ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) = ( 1r𝑅 ) )
632 615 631 oveq12d ( ( 𝜑𝑙 = 0 ) → ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) = ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) )
633 oveq2 ( 𝑙 = 0 → ( 𝐻𝑙 ) = ( 𝐻 − 0 ) )
634 633 adantl ( ( 𝜑𝑙 = 0 ) → ( 𝐻𝑙 ) = ( 𝐻 − 0 ) )
635 294 adantr ( ( 𝜑𝑙 = 0 ) → 𝐻 ∈ ℂ )
636 635 subid1d ( ( 𝜑𝑙 = 0 ) → ( 𝐻 − 0 ) = 𝐻 )
637 634 636 eqtrd ( ( 𝜑𝑙 = 0 ) → ( 𝐻𝑙 ) = 𝐻 )
638 637 oveq1d ( ( 𝜑𝑙 = 0 ) → ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) = ( 𝐻 ( .g𝑀 ) 𝑋 ) )
639 632 638 oveq12d ( ( 𝜑𝑙 = 0 ) → ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) )
640 31 193 98 601 613 639 gsummptfzsplitla ( 𝜑 → ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) = ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( 𝑊 Σg ( 𝑙 ∈ ( ( 0 + 1 ) ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ) )
641 0p1e1 ( 0 + 1 ) = 1
642 641 oveq1i ( ( 0 + 1 ) ... ( ♯ ‘ 𝐽 ) ) = ( 1 ... ( ♯ ‘ 𝐽 ) )
643 642 mpteq1i ( 𝑙 ∈ ( ( 0 + 1 ) ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) = ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) )
644 643 oveq2i ( 𝑊 Σg ( 𝑙 ∈ ( ( 0 + 1 ) ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) )
645 644 oveq2i ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( 𝑊 Σg ( 𝑙 ∈ ( ( 0 + 1 ) ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ) = ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) )
646 645 a1i ( 𝜑 → ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( 𝑊 Σg ( 𝑙 ∈ ( ( 0 + 1 ) ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ) = ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ) )
647 43 ringabld ( 𝜑𝑊 ∈ Abel )
648 fzfid ( 𝜑 → ( 1 ... ( ♯ ‘ 𝐽 ) ) ∈ Fin )
649 541 ralrimiva ( 𝜑 → ∀ 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) )
650 31 98 648 649 gsummptcl ( 𝜑 → ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ∈ ( Base ‘ 𝑊 ) )
651 31 193 647 252 650 ablcomd ( 𝜑 → ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ) = ( ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ) )
652 640 646 651 3eqtrd ( 𝜑 → ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) = ( ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ) )
653 600 652 eqtr3d ( 𝜑 → ( 𝑊 Σg ( 𝑙 ∈ ( 0 ..^ 𝐻 ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) = ( ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ) )
654 653 oveq1d ( 𝜑 → ( ( 𝑊 Σg ( 𝑙 ∈ ( 0 ..^ 𝐻 ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) = ( ( ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ) ( +g𝑊 ) ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) )
655 593 654 eqtr2d ( 𝜑 → ( ( ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ) ( +g𝑊 ) ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) )
656 31 193 44 650 252 264 grpassd ( 𝜑 → ( ( ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ) ( +g𝑊 ) ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) = ( ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) ) )
657 561 655 656 3eqtr2rd ( 𝜑 → ( ( 𝑊 Σg ( 𝑙 ∈ ( 1 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( 𝑙 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑙 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑙 ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) ) = ( 𝑊 Σg ( 𝑘 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) ) )
658 46 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → 𝑅 ∈ Ring )
659 658 151 syl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
660 566 sselda ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → 𝑘 ∈ ℕ0 )
661 158 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → ( 𝑁1 ) ∈ 𝐵 )
662 150 12 659 660 661 mulgnn0cld ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → ( 𝑘 ( 𝑁1 ) ) ∈ 𝐵 )
663 14 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → 𝐼 ∈ Fin )
664 35 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → 𝑅 ∈ CRing )
665 6 fveq1i ( 𝐸𝑘 ) = ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝑘 )
666 257 663 658 660 255 esplympl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝑘 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
667 665 666 eqeltrid ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → ( 𝐸𝑘 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
668 260 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → 𝑍 ∈ ( 𝐵m 𝐼 ) )
669 5 254 255 2 663 664 667 668 evlcl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) ∈ 𝐵 )
670 2 9 658 662 669 ringcld ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → ( ( 𝑘 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) ) ∈ 𝐵 )
671 117 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → 𝑀 ∈ Mnd )
672 fznn0sub2 ( 𝑘 ∈ ( 0 ... 𝐻 ) → ( 𝐻𝑘 ) ∈ ( 0 ... 𝐻 ) )
673 672 adantl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → ( 𝐻𝑘 ) ∈ ( 0 ... 𝐻 ) )
674 414 673 sselid ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → ( 𝐻𝑘 ) ∈ ℕ0 )
675 48 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
676 32 81 671 674 675 mulgnn0cld ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → ( ( 𝐻𝑘 ) ( .g𝑀 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
677 1 31 2 80 658 670 676 ply1vscl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐻 ) ) → ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑘 ) ( .g𝑀 ) 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) )
678 oveq1 ( 𝑘 = ( 𝐻𝑙 ) → ( 𝑘 ( 𝑁1 ) ) = ( ( 𝐻𝑙 ) ( 𝑁1 ) ) )
679 2fveq3 ( 𝑘 = ( 𝐻𝑙 ) → ( 𝑄 ‘ ( 𝐸𝑘 ) ) = ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) )
680 679 fveq1d ( 𝑘 = ( 𝐻𝑙 ) → ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) )
681 678 680 oveq12d ( 𝑘 = ( 𝐻𝑙 ) → ( ( 𝑘 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) ) = ( ( ( 𝐻𝑙 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ) )
682 681 adantl ( ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) ∧ 𝑘 = ( 𝐻𝑙 ) ) → ( ( 𝑘 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) ) = ( ( ( 𝐻𝑙 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ) )
683 simpr ( ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) ∧ 𝑘 = ( 𝐻𝑙 ) ) → 𝑘 = ( 𝐻𝑙 ) )
684 683 oveq2d ( ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) ∧ 𝑘 = ( 𝐻𝑙 ) ) → ( 𝐻𝑘 ) = ( 𝐻 − ( 𝐻𝑙 ) ) )
685 294 ad2antrr ( ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) ∧ 𝑘 = ( 𝐻𝑙 ) ) → 𝐻 ∈ ℂ )
686 567 adantr ( ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) ∧ 𝑘 = ( 𝐻𝑙 ) ) → 𝑙 ∈ ℕ0 )
687 686 nn0cnd ( ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) ∧ 𝑘 = ( 𝐻𝑙 ) ) → 𝑙 ∈ ℂ )
688 685 687 nncand ( ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) ∧ 𝑘 = ( 𝐻𝑙 ) ) → ( 𝐻 − ( 𝐻𝑙 ) ) = 𝑙 )
689 684 688 eqtrd ( ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) ∧ 𝑘 = ( 𝐻𝑙 ) ) → ( 𝐻𝑘 ) = 𝑙 )
690 689 oveq1d ( ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) ∧ 𝑘 = ( 𝐻𝑙 ) ) → ( ( 𝐻𝑘 ) ( .g𝑀 ) 𝑋 ) = ( 𝑙 ( .g𝑀 ) 𝑋 ) )
691 682 690 oveq12d ( ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) ∧ 𝑘 = ( 𝐻𝑙 ) ) → ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑘 ) ( .g𝑀 ) 𝑋 ) ) = ( ( ( ( 𝐻𝑙 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) )
692 31 98 250 677 691 gsummptrev ( 𝜑 → ( 𝑊 Σg ( 𝑘 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( 𝑘 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝑘 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻𝑘 ) ( .g𝑀 ) 𝑋 ) ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( ( 𝐻𝑙 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) )
693 551 657 692 3eqtrd ( 𝜑 → ( ( 𝑊 Σg ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( ( 𝑘 + 1 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( ( 𝐻 − ( 𝑘 + 1 ) ) ( .g𝑀 ) 𝑋 ) ) ) ) ( +g𝑊 ) ( ( ( ( 0 ( 𝑁1 ) ) · ( 1r𝑅 ) ) ( ·𝑠𝑊 ) ( 𝐻 ( .g𝑀 ) 𝑋 ) ) ( +g𝑊 ) ( ( ( 𝐻 ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸𝐻 ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 0 ( .g𝑀 ) 𝑋 ) ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( ( 𝐻𝑙 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) )
694 479 513 693 3eqtr3d ( 𝜑 → ( ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) ↦ ( ( ( ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ( 𝑁1 ) ) · ( ( ( 𝐽 eval 𝑅 ) ‘ ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ 𝐽 ) − 𝑙 ) ) ) ‘ ( 𝑍𝐽 ) ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) ( .r𝑊 ) ( 𝑋 ( 𝐴 ‘ ( 𝑍𝑌 ) ) ) ) = ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( ( 𝐻𝑙 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) )
695 79 192 694 3eqtrd ( 𝜑𝐹 = ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( ( 𝐻𝑙 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) )
696 695 fveq2d ( 𝜑 → ( coe1𝐹 ) = ( coe1 ‘ ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( ( 𝐻𝑙 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) ) )
697 696 fveq1d ( 𝜑 → ( ( coe1𝐹 ) ‘ 𝐾 ) = ( ( coe1 ‘ ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( ( 𝐻𝑙 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) ) ‘ 𝐾 ) )
698 4 fveq2i ( .g𝑀 ) = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
699 150 12 565 579 568 mulgnn0cld ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( ( 𝐻𝑙 ) ( 𝑁1 ) ) ∈ 𝐵 )
700 6 fveq1i ( 𝐸 ‘ ( 𝐻𝑙 ) ) = ( ( 𝐼 eSymPoly 𝑅 ) ‘ ( 𝐻𝑙 ) )
701 257 570 564 579 255 esplympl ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ ( 𝐻𝑙 ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
702 700 701 eqeltrid ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( 𝐸 ‘ ( 𝐻𝑙 ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
703 5 254 255 2 570 571 702 574 evlcl ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ∈ 𝐵 )
704 2 9 564 699 703 ringcld ( ( 𝜑𝑙 ∈ ( 0 ... 𝐻 ) ) → ( ( ( 𝐻𝑙 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ) ∈ 𝐵 )
705 704 ralrimiva ( 𝜑 → ∀ 𝑙 ∈ ( 0 ... 𝐻 ) ( ( ( 𝐻𝑙 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ) ∈ 𝐵 )
706 oveq2 ( 𝑙 = 𝐾 → ( 𝐻𝑙 ) = ( 𝐻𝐾 ) )
707 706 oveq1d ( 𝑙 = 𝐾 → ( ( 𝐻𝑙 ) ( 𝑁1 ) ) = ( ( 𝐻𝐾 ) ( 𝑁1 ) ) )
708 706 fveq2d ( 𝑙 = 𝐾 → ( 𝐸 ‘ ( 𝐻𝑙 ) ) = ( 𝐸 ‘ ( 𝐻𝐾 ) ) )
709 708 fveq2d ( 𝑙 = 𝐾 → ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) = ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝐾 ) ) ) )
710 709 fveq1d ( 𝑙 = 𝐾 → ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝐾 ) ) ) ‘ 𝑍 ) )
711 707 710 oveq12d ( 𝑙 = 𝐾 → ( ( ( 𝐻𝑙 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ) = ( ( ( 𝐻𝐾 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝐾 ) ) ) ‘ 𝑍 ) ) )
712 1 31 10 698 46 2 80 250 705 18 711 gsummoncoe1fz ( 𝜑 → ( ( coe1 ‘ ( 𝑊 Σg ( 𝑙 ∈ ( 0 ... 𝐻 ) ↦ ( ( ( ( 𝐻𝑙 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝑙 ) ) ) ‘ 𝑍 ) ) ( ·𝑠𝑊 ) ( 𝑙 ( .g𝑀 ) 𝑋 ) ) ) ) ) ‘ 𝐾 ) = ( ( ( 𝐻𝐾 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝐾 ) ) ) ‘ 𝑍 ) ) )
713 697 712 eqtrd ( 𝜑 → ( ( coe1𝐹 ) ‘ 𝐾 ) = ( ( ( 𝐻𝐾 ) ( 𝑁1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐻𝐾 ) ) ) ‘ 𝑍 ) ) )