This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vieta

Description: Vieta's Formulas: Coefficients of a monic polynomial F expressed as a product of linear polynomials of the form X - Z can be expressed in terms of elementary symmetric polynomials. The formulas appear in Chapter 6 of Lang, p. 190. Theorem vieta1 is a special case for the complex numbers, for the case K = 1 . (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 ... 𝐻 ) )
vieta.c ⊢ 𝐶 = ( coe1 ‘ 𝐹 )
Assertion vieta ( 𝜑 → ( 𝐶 ‘ ( 𝐻 − 𝐾 ) ) = ( ( 𝐾 ↑ ( 𝑁 ‘ 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 vieta.c ⊢ 𝐶 = ( coe1 ‘ 𝐹 )
20 fveq1 ⊢ ( 𝑧 = 𝑍 → ( 𝑧 ‘ 𝑛 ) = ( 𝑍 ‘ 𝑛 ) )
21 20 fveq2d ⊢ ( 𝑧 = 𝑍 → ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) = ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) )
22 21 oveq2d ⊢ ( 𝑧 = 𝑍 → ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) = ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) )
23 22 mpteq2dv ⊢ ( 𝑧 = 𝑍 → ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) )
24 23 oveq2d ⊢ ( 𝑧 = 𝑍 → ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) = ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) ) )
25 24 17 eqtr4di ⊢ ( 𝑧 = 𝑍 → ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) = 𝐹 )
26 25 fveq2d ⊢ ( 𝑧 = 𝑍 → ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) = ( coe1 ‘ 𝐹 ) )
27 26 19 eqtr4di ⊢ ( 𝑧 = 𝑍 → ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) = 𝐶 )
28 27 fveq1d ⊢ ( 𝑧 = 𝑍 → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( 𝐻 − 𝑘 ) ) = ( 𝐶 ‘ ( 𝐻 − 𝑘 ) ) )
29 fveq2 ⊢ ( 𝑧 = 𝑍 → ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑧 ) = ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑍 ) )
30 29 oveq2d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑍 ) ) )
31 28 30 eqeq12d ⊢ ( 𝑧 = 𝑍 → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( 𝐻 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( 𝐶 ‘ ( 𝐻 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑍 ) ) ) )
32 oveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝐻 − 𝑘 ) = ( 𝐻 − 𝐾 ) )
33 32 fveq2d ⊢ ( 𝑘 = 𝐾 → ( 𝐶 ‘ ( 𝐻 − 𝑘 ) ) = ( 𝐶 ‘ ( 𝐻 − 𝐾 ) ) )
34 oveq1 ⊢ ( 𝑘 = 𝐾 → ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) = ( 𝐾 ↑ ( 𝑁 ‘ 1 ) ) )
35 2fveq3 ⊢ ( 𝑘 = 𝐾 → ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) = ( 𝑄 ‘ ( 𝐸 ‘ 𝐾 ) ) )
36 35 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( 𝐸 ‘ 𝐾 ) ) ‘ 𝑍 ) )
37 34 36 oveq12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑍 ) ) = ( ( 𝐾 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝐾 ) ) ‘ 𝑍 ) ) )
38 33 37 eqeq12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝐶 ‘ ( 𝐻 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑍 ) ) ↔ ( 𝐶 ‘ ( 𝐻 − 𝐾 ) ) = ( ( 𝐾 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝐾 ) ) ‘ 𝑍 ) ) ) )
39 oveq2 ⊢ ( 𝑗 = ∅ → ( 𝐵 ↑m 𝑗 ) = ( 𝐵 ↑m ∅ ) )
40 2 fvexi ⊢ 𝐵 ∈ V
41 mapdm0 ⊢ ( 𝐵 ∈ V → ( 𝐵 ↑m ∅ ) = { ∅ } )
42 40 41 ax-mp ⊢ ( 𝐵 ↑m ∅ ) = { ∅ }
43 39 42 eqtrdi ⊢ ( 𝑗 = ∅ → ( 𝐵 ↑m 𝑗 ) = { ∅ } )
44 fveq2 ⊢ ( 𝑗 = ∅ → ( ♯ ‘ 𝑗 ) = ( ♯ ‘ ∅ ) )
45 44 oveq2d ⊢ ( 𝑗 = ∅ → ( 0 ... ( ♯ ‘ 𝑗 ) ) = ( 0 ... ( ♯ ‘ ∅ ) ) )
46 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
47 46 oveq2i ⊢ ( 0 ... ( ♯ ‘ ∅ ) ) = ( 0 ... 0 )
48 fz0sn ⊢ ( 0 ... 0 ) = { 0 }
49 47 48 eqtri ⊢ ( 0 ... ( ♯ ‘ ∅ ) ) = { 0 }
50 45 49 eqtrdi ⊢ ( 𝑗 = ∅ → ( 0 ... ( ♯ ‘ 𝑗 ) ) = { 0 } )
51 mpteq1 ⊢ ( 𝑗 = ∅ → ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ ∅ ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) )
52 mpt0 ⊢ ( 𝑛 ∈ ∅ ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) = ∅
53 51 52 eqtrdi ⊢ ( 𝑗 = ∅ → ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) = ∅ )
54 53 oveq2d ⊢ ( 𝑗 = ∅ → ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) = ( 𝑀 Σg ∅ ) )
55 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
56 55 gsum0 ⊢ ( 𝑀 Σg ∅ ) = ( 0g ‘ 𝑀 )
57 54 56 eqtrdi ⊢ ( 𝑗 = ∅ → ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) = ( 0g ‘ 𝑀 ) )
58 57 fveq2d ⊢ ( 𝑗 = ∅ → ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) = ( coe1 ‘ ( 0g ‘ 𝑀 ) ) )
59 44 oveq1d ⊢ ( 𝑗 = ∅ → ( ( ♯ ‘ 𝑗 ) − 𝑘 ) = ( ( ♯ ‘ ∅ ) − 𝑘 ) )
60 46 oveq1i ⊢ ( ( ♯ ‘ ∅ ) − 𝑘 ) = ( 0 − 𝑘 )
61 59 60 eqtrdi ⊢ ( 𝑗 = ∅ → ( ( ♯ ‘ 𝑗 ) − 𝑘 ) = ( 0 − 𝑘 ) )
62 58 61 fveq12d ⊢ ( 𝑗 = ∅ → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) )
63 oveq1 ⊢ ( 𝑗 = ∅ → ( 𝑗 eval 𝑅 ) = ( ∅ eval 𝑅 ) )
64 oveq1 ⊢ ( 𝑗 = ∅ → ( 𝑗 eSymPoly 𝑅 ) = ( ∅ eSymPoly 𝑅 ) )
65 64 fveq1d ⊢ ( 𝑗 = ∅ → ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) = ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) )
66 63 65 fveq12d ⊢ ( 𝑗 = ∅ → ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) = ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) )
67 66 fveq1d ⊢ ( 𝑗 = ∅ → ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) = ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) )
68 67 oveq2d ⊢ ( 𝑗 = ∅ → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
69 62 68 eqeq12d ⊢ ( 𝑗 = ∅ → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
70 50 69 raleqbidv ⊢ ( 𝑗 = ∅ → ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑗 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
71 43 70 raleqbidv ⊢ ( 𝑗 = ∅ → ( ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑗 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑗 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ { ∅ } ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
72 oveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐵 ↑m 𝑗 ) = ( 𝐵 ↑m 𝑖 ) )
73 fveq2 ⊢ ( 𝑗 = 𝑖 → ( ♯ ‘ 𝑗 ) = ( ♯ ‘ 𝑖 ) )
74 73 oveq2d ⊢ ( 𝑗 = 𝑖 → ( 0 ... ( ♯ ‘ 𝑗 ) ) = ( 0 ... ( ♯ ‘ 𝑖 ) ) )
75 mpteq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) )
76 75 oveq2d ⊢ ( 𝑗 = 𝑖 → ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) = ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) )
77 76 fveq2d ⊢ ( 𝑗 = 𝑖 → ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) = ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) )
78 73 oveq1d ⊢ ( 𝑗 = 𝑖 → ( ( ♯ ‘ 𝑗 ) − 𝑘 ) = ( ( ♯ ‘ 𝑖 ) − 𝑘 ) )
79 77 78 fveq12d ⊢ ( 𝑗 = 𝑖 → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) )
80 oveq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑗 eval 𝑅 ) = ( 𝑖 eval 𝑅 ) )
81 oveq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑗 eSymPoly 𝑅 ) = ( 𝑖 eSymPoly 𝑅 ) )
82 81 fveq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) = ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) )
83 80 82 fveq12d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) = ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) )
84 83 fveq1d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) = ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) )
85 84 oveq2d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
86 79 85 eqeq12d ⊢ ( 𝑗 = 𝑖 → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
87 74 86 raleqbidv ⊢ ( 𝑗 = 𝑖 → ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑗 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
88 72 87 raleqbidv ⊢ ( 𝑗 = 𝑖 → ( ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑗 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑗 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
89 oveq2 ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( 𝐵 ↑m 𝑗 ) = ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) )
90 fveq2 ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( ♯ ‘ 𝑗 ) = ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) )
91 90 oveq2d ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( 0 ... ( ♯ ‘ 𝑗 ) ) = ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) )
92 mpteq1 ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) )
93 92 oveq2d ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) = ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) )
94 93 fveq2d ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) = ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) )
95 90 oveq1d ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( ( ♯ ‘ 𝑗 ) − 𝑘 ) = ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) )
96 94 95 fveq12d ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) )
97 oveq1 ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( 𝑗 eval 𝑅 ) = ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) )
98 oveq1 ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( 𝑗 eSymPoly 𝑅 ) = ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) )
99 98 fveq1d ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) = ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) )
100 97 99 fveq12d ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) = ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) )
101 100 fveq1d ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) = ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) )
102 101 oveq2d ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
103 96 102 eqeq12d ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
104 91 103 raleqbidv ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑗 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
105 89 104 raleqbidv ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑚 } ) → ( ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑗 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑗 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
106 oveq2 ⊢ ( 𝑗 = 𝐼 → ( 𝐵 ↑m 𝑗 ) = ( 𝐵 ↑m 𝐼 ) )
107 fveq2 ⊢ ( 𝑗 = 𝐼 → ( ♯ ‘ 𝑗 ) = ( ♯ ‘ 𝐼 ) )
108 107 13 eqtr4di ⊢ ( 𝑗 = 𝐼 → ( ♯ ‘ 𝑗 ) = 𝐻 )
109 108 oveq2d ⊢ ( 𝑗 = 𝐼 → ( 0 ... ( ♯ ‘ 𝑗 ) ) = ( 0 ... 𝐻 ) )
110 mpteq1 ⊢ ( 𝑗 = 𝐼 → ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) )
111 110 oveq2d ⊢ ( 𝑗 = 𝐼 → ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) = ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) )
112 111 fveq2d ⊢ ( 𝑗 = 𝐼 → ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) = ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) )
113 108 oveq1d ⊢ ( 𝑗 = 𝐼 → ( ( ♯ ‘ 𝑗 ) − 𝑘 ) = ( 𝐻 − 𝑘 ) )
114 112 113 fveq12d ⊢ ( 𝑗 = 𝐼 → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( 𝐻 − 𝑘 ) ) )
115 oveq1 ⊢ ( 𝑗 = 𝐼 → ( 𝑗 eval 𝑅 ) = ( 𝐼 eval 𝑅 ) )
116 115 5 eqtr4di ⊢ ( 𝑗 = 𝐼 → ( 𝑗 eval 𝑅 ) = 𝑄 )
117 oveq1 ⊢ ( 𝑗 = 𝐼 → ( 𝑗 eSymPoly 𝑅 ) = ( 𝐼 eSymPoly 𝑅 ) )
118 117 6 eqtr4di ⊢ ( 𝑗 = 𝐼 → ( 𝑗 eSymPoly 𝑅 ) = 𝐸 )
119 118 fveq1d ⊢ ( 𝑗 = 𝐼 → ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) = ( 𝐸 ‘ 𝑘 ) )
120 116 119 fveq12d ⊢ ( 𝑗 = 𝐼 → ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) = ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) )
121 120 fveq1d ⊢ ( 𝑗 = 𝐼 → ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) = ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑧 ) )
122 121 oveq2d ⊢ ( 𝑗 = 𝐼 → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
123 114 122 eqeq12d ⊢ ( 𝑗 = 𝐼 → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( 𝐻 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
124 109 123 raleqbidv ⊢ ( 𝑗 = 𝐼 → ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑗 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑘 ∈ ( 0 ... 𝐻 ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( 𝐻 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
125 106 124 raleqbidv ⊢ ( 𝑗 = 𝐼 → ( ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑗 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑗 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑗 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑗 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑗 eval 𝑅 ) ‘ ( ( 𝑗 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝐼 ) ∀ 𝑘 ∈ ( 0 ... 𝐻 ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( 𝐻 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
126 15 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
127 2 8 126 ringidcld ⊢ ( 𝜑 → 1 ∈ 𝐵 )
128 2 9 8 126 127 ringlidmd ⊢ ( 𝜑 → ( 1 · 1 ) = 1 )
129 126 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
130 2 7 129 127 grpinvcld ⊢ ( 𝜑 → ( 𝑁 ‘ 1 ) ∈ 𝐵 )
131 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
132 131 2 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
133 131 8 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
134 132 133 12 mulg0 ⊢ ( ( 𝑁 ‘ 1 ) ∈ 𝐵 → ( 0 ↑ ( 𝑁 ‘ 1 ) ) = 1 )
135 130 134 syl ⊢ ( 𝜑 → ( 0 ↑ ( 𝑁 ‘ 1 ) ) = 1 )
136 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
137 136 8 zrh1 ⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = 1 )
138 126 137 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = 1 )
139 138 sneqd ⊢ ( 𝜑 → { ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) } = { 1 } )
140 139 xpeq2d ⊢ ( 𝜑 → ( { ∅ } × { ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) } ) = ( { ∅ } × { 1 } ) )
141 0ex ⊢ ∅ ∈ V
142 141 a1i ⊢ ( 𝜑 → ∅ ∈ V )
143 8 fvexi ⊢ 1 ∈ V
144 143 a1i ⊢ ( 𝜑 → 1 ∈ V )
145 xpsng ⊢ ( ( ∅ ∈ V ∧ 1 ∈ V ) → ( { ∅ } × { 1 } ) = { ⟨ ∅ , 1 ⟩ } )
146 142 144 145 syl2anc ⊢ ( 𝜑 → ( { ∅ } × { 1 } ) = { ⟨ ∅ , 1 ⟩ } )
147 0xp ⊢ ( ∅ × { 0 } ) = ∅
148 147 eqcomi ⊢ ∅ = ( ∅ × { 0 } )
149 148 eqeq2i ⊢ ( 𝑓 = ∅ ↔ 𝑓 = ( ∅ × { 0 } ) )
150 149 biimpi ⊢ ( 𝑓 = ∅ → 𝑓 = ( ∅ × { 0 } ) )
151 150 adantl ⊢ ( ( 𝜑 ∧ 𝑓 = ∅ ) → 𝑓 = ( ∅ × { 0 } ) )
152 151 iftrued ⊢ ( ( 𝜑 ∧ 𝑓 = ∅ ) → if ( 𝑓 = ( ∅ × { 0 } ) , 1 , ( 0g ‘ 𝑅 ) ) = 1 )
153 152 142 144 fmptsnd ⊢ ( 𝜑 → { ⟨ ∅ , 1 ⟩ } = ( 𝑓 ∈ { ∅ } ↦ if ( 𝑓 = ( ∅ × { 0 } ) , 1 , ( 0g ‘ 𝑅 ) ) ) )
154 140 146 153 3eqtrd ⊢ ( 𝜑 → ( { ∅ } × { ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) } ) = ( 𝑓 ∈ { ∅ } ↦ if ( 𝑓 = ( ∅ × { 0 } ) , 1 , ( 0g ‘ 𝑅 ) ) ) )
155 elsni ⊢ ( ℎ ∈ { ∅ } → ℎ = ∅ )
156 nn0ex ⊢ ℕ0 ∈ V
157 mapdm0 ⊢ ( ℕ0 ∈ V → ( ℕ0 ↑m ∅ ) = { ∅ } )
158 156 157 ax-mp ⊢ ( ℕ0 ↑m ∅ ) = { ∅ }
159 155 158 eleq2s ⊢ ( ℎ ∈ ( ℕ0 ↑m ∅ ) → ℎ = ∅ )
160 159 cnveqd ⊢ ( ℎ ∈ ( ℕ0 ↑m ∅ ) → ◡ ℎ = ◡ ∅ )
161 160 imaeq1d ⊢ ( ℎ ∈ ( ℕ0 ↑m ∅ ) → ( ◡ ℎ “ ℕ ) = ( ◡ ∅ “ ℕ ) )
162 cnv0 ⊢ ◡ ∅ = ∅
163 162 imaeq1i ⊢ ( ◡ ∅ “ ℕ ) = ( ∅ “ ℕ )
164 0ima ⊢ ( ∅ “ ℕ ) = ∅
165 163 164 eqtri ⊢ ( ◡ ∅ “ ℕ ) = ∅
166 161 165 eqtrdi ⊢ ( ℎ ∈ ( ℕ0 ↑m ∅ ) → ( ◡ ℎ “ ℕ ) = ∅ )
167 0fi ⊢ ∅ ∈ Fin
168 166 167 eqeltrdi ⊢ ( ℎ ∈ ( ℕ0 ↑m ∅ ) → ( ◡ ℎ “ ℕ ) ∈ Fin )
169 168 rabeqc ⊢ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = ( ℕ0 ↑m ∅ )
170 169 158 eqtr2i ⊢ { ∅ } = { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
171 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 }
172 171 psrbasfsupp ⊢ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
173 170 172 eqtr4i ⊢ { ∅ } = { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 }
174 0nn0 ⊢ 0 ∈ ℕ0
175 174 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
176 173 142 15 175 esplyfval ⊢ ( 𝜑 → ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ { ∅ } ) ‘ ( ( 𝟭 ‘ ∅ ) “ { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) ) )
177 fveqeq2 ⊢ ( 𝑐 = ∅ → ( ( ♯ ‘ 𝑐 ) = 0 ↔ ( ♯ ‘ ∅ ) = 0 ) )
178 0elpw ⊢ ∅ ∈ 𝒫 ∅
179 178 a1i ⊢ ( 𝜑 → ∅ ∈ 𝒫 ∅ )
180 46 a1i ⊢ ( 𝜑 → ( ♯ ‘ ∅ ) = 0 )
181 hasheq0 ⊢ ( 𝑐 ∈ 𝒫 ∅ → ( ( ♯ ‘ 𝑐 ) = 0 ↔ 𝑐 = ∅ ) )
182 181 biimpa ⊢ ( ( 𝑐 ∈ 𝒫 ∅ ∧ ( ♯ ‘ 𝑐 ) = 0 ) → 𝑐 = ∅ )
183 182 adantll ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 ∅ ) ∧ ( ♯ ‘ 𝑐 ) = 0 ) → 𝑐 = ∅ )
184 177 179 180 183 rabeqsnd ⊢ ( 𝜑 → { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } = { ∅ } )
185 184 imaeq2d ⊢ ( 𝜑 → ( ( 𝟭 ‘ ∅ ) “ { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } ) = ( ( 𝟭 ‘ ∅ ) “ { ∅ } ) )
186 pw0 ⊢ 𝒫 ∅ = { ∅ }
187 186 a1i ⊢ ( 𝜑 → 𝒫 ∅ = { ∅ } )
188 indf1o ⊢ ( ∅ ∈ V → ( 𝟭 ‘ ∅ ) : 𝒫 ∅ –1-1-onto→ ( { 0 , 1 } ↑m ∅ ) )
189 f1of ⊢ ( ( 𝟭 ‘ ∅ ) : 𝒫 ∅ –1-1-onto→ ( { 0 , 1 } ↑m ∅ ) → ( 𝟭 ‘ ∅ ) : 𝒫 ∅ ⟶ ( { 0 , 1 } ↑m ∅ ) )
190 142 188 189 3syl ⊢ ( 𝜑 → ( 𝟭 ‘ ∅ ) : 𝒫 ∅ ⟶ ( { 0 , 1 } ↑m ∅ ) )
191 187 190 feq2dd ⊢ ( 𝜑 → ( 𝟭 ‘ ∅ ) : { ∅ } ⟶ ( { 0 , 1 } ↑m ∅ ) )
192 191 ffnd ⊢ ( 𝜑 → ( 𝟭 ‘ ∅ ) Fn { ∅ } )
193 141 snid ⊢ ∅ ∈ { ∅ }
194 193 a1i ⊢ ( 𝜑 → ∅ ∈ { ∅ } )
195 192 194 fnimasnd ⊢ ( 𝜑 → ( ( 𝟭 ‘ ∅ ) “ { ∅ } ) = { ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) } )
196 ssidd ⊢ ( 𝜑 → ∅ ⊆ ∅ )
197 indf ⊢ ( ( ∅ ∈ V ∧ ∅ ⊆ ∅ ) → ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) : ∅ ⟶ { 0 , 1 } )
198 142 196 197 syl2anc ⊢ ( 𝜑 → ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) : ∅ ⟶ { 0 , 1 } )
199 f0bi ⊢ ( ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) : ∅ ⟶ { 0 , 1 } ↔ ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) = ∅ )
200 198 199 sylib ⊢ ( 𝜑 → ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) = ∅ )
201 200 sneqd ⊢ ( 𝜑 → { ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) } = { ∅ } )
202 185 195 201 3eqtrd ⊢ ( 𝜑 → ( ( 𝟭 ‘ ∅ ) “ { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } ) = { ∅ } )
203 202 fveq2d ⊢ ( 𝜑 → ( ( 𝟭 ‘ { ∅ } ) ‘ ( ( 𝟭 ‘ ∅ ) “ { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) = ( ( 𝟭 ‘ { ∅ } ) ‘ { ∅ } ) )
204 p0ex ⊢ { ∅ } ∈ V
205 indconst1 ⊢ ( { ∅ } ∈ V → ( ( 𝟭 ‘ { ∅ } ) ‘ { ∅ } ) = ( { ∅ } × { 1 } ) )
206 204 205 ax-mp ⊢ ( ( 𝟭 ‘ { ∅ } ) ‘ { ∅ } ) = ( { ∅ } × { 1 } )
207 203 206 eqtrdi ⊢ ( 𝜑 → ( ( 𝟭 ‘ { ∅ } ) ‘ ( ( 𝟭 ‘ ∅ ) “ { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) = ( { ∅ } × { 1 } ) )
208 207 coeq2d ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ { ∅ } ) ‘ ( ( 𝟭 ‘ ∅ ) “ { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( { ∅ } × { 1 } ) ) )
209 136 zrhrhm ⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
210 zringbas ⊢ ℤ = ( Base ‘ ℤring )
211 210 2 rhmf ⊢ ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ 𝐵 )
212 126 209 211 3syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ 𝐵 )
213 212 ffnd ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) Fn ℤ )
214 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
215 fcoconst ⊢ ( ( ( ℤRHom ‘ 𝑅 ) Fn ℤ ∧ 1 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( { ∅ } × { 1 } ) ) = ( { ∅ } × { ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) } ) )
216 213 214 215 syl2anc ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( { ∅ } × { 1 } ) ) = ( { ∅ } × { ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) } ) )
217 176 208 216 3eqtrd ⊢ ( 𝜑 → ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) = ( { ∅ } × { ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) } ) )
218 eqid ⊢ ( ∅ mPoly 𝑅 ) = ( ∅ mPoly 𝑅 )
219 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
220 eqid ⊢ ( algSc ‘ ( ∅ mPoly 𝑅 ) ) = ( algSc ‘ ( ∅ mPoly 𝑅 ) )
221 218 170 219 2 220 142 126 127 mplascl ⊢ ( 𝜑 → ( ( algSc ‘ ( ∅ mPoly 𝑅 ) ) ‘ 1 ) = ( 𝑓 ∈ { ∅ } ↦ if ( 𝑓 = ( ∅ × { 0 } ) , 1 , ( 0g ‘ 𝑅 ) ) ) )
222 154 217 221 3eqtr4d ⊢ ( 𝜑 → ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) = ( ( algSc ‘ ( ∅ mPoly 𝑅 ) ) ‘ 1 ) )
223 222 fveq2d ⊢ ( 𝜑 → ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) = ( ( ∅ eval 𝑅 ) ‘ ( ( algSc ‘ ( ∅ mPoly 𝑅 ) ) ‘ 1 ) ) )
224 223 fveq1d ⊢ ( 𝜑 → ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) = ( ( ( ∅ eval 𝑅 ) ‘ ( ( algSc ‘ ( ∅ mPoly 𝑅 ) ) ‘ 1 ) ) ‘ ∅ ) )
225 eqid ⊢ ( ∅ eval 𝑅 ) = ( ∅ eval 𝑅 )
226 193 158 eleqtrri ⊢ ∅ ∈ ( ℕ0 ↑m ∅ )
227 226 a1i ⊢ ( 𝜑 → ∅ ∈ ( ℕ0 ↑m ∅ ) )
228 15 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
229 225 218 2 220 227 228 127 evlsca ⊢ ( 𝜑 → ( ( ∅ eval 𝑅 ) ‘ ( ( algSc ‘ ( ∅ mPoly 𝑅 ) ) ‘ 1 ) ) = ( ( 𝐵 ↑m ∅ ) × { 1 } ) )
230 229 fveq1d ⊢ ( 𝜑 → ( ( ( ∅ eval 𝑅 ) ‘ ( ( algSc ‘ ( ∅ mPoly 𝑅 ) ) ‘ 1 ) ) ‘ ∅ ) = ( ( ( 𝐵 ↑m ∅ ) × { 1 } ) ‘ ∅ ) )
231 193 42 eleqtrri ⊢ ∅ ∈ ( 𝐵 ↑m ∅ )
232 143 fvconst2 ⊢ ( ∅ ∈ ( 𝐵 ↑m ∅ ) → ( ( ( 𝐵 ↑m ∅ ) × { 1 } ) ‘ ∅ ) = 1 )
233 231 232 mp1i ⊢ ( 𝜑 → ( ( ( 𝐵 ↑m ∅ ) × { 1 } ) ‘ ∅ ) = 1 )
234 224 230 233 3eqtrd ⊢ ( 𝜑 → ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) = 1 )
235 135 234 oveq12d ⊢ ( 𝜑 → ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) = ( 1 · 1 ) )
236 iftrue ⊢ ( 𝑙 = 0 → if ( 𝑙 = 0 , 1 , ( 0g ‘ 𝑅 ) ) = 1 )
237 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
238 4 237 ringidval ⊢ ( 1r ‘ 𝑊 ) = ( 0g ‘ 𝑀 )
239 238 eqcomi ⊢ ( 0g ‘ 𝑀 ) = ( 1r ‘ 𝑊 )
240 1 239 219 8 coe1id ⊢ ( 𝑅 ∈ Ring → ( coe1 ‘ ( 0g ‘ 𝑀 ) ) = ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , 1 , ( 0g ‘ 𝑅 ) ) ) )
241 126 240 syl ⊢ ( 𝜑 → ( coe1 ‘ ( 0g ‘ 𝑀 ) ) = ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , 1 , ( 0g ‘ 𝑅 ) ) ) )
242 236 241 175 144 fvmptd4 ⊢ ( 𝜑 → ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) = 1 )
243 128 235 242 3eqtr4rd ⊢ ( 𝜑 → ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) = ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) )
244 fveq2 ⊢ ( 𝑧 = ∅ → ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) = ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) )
245 244 oveq2d ⊢ ( 𝑧 = ∅ → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) ) )
246 245 eqeq2d ⊢ ( 𝑧 = ∅ → ( ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) ) ) )
247 246 ralbidv ⊢ ( 𝑧 = ∅ → ( ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) ) ) )
248 c0ex ⊢ 0 ∈ V
249 oveq2 ⊢ ( 𝑘 = 0 → ( 0 − 𝑘 ) = ( 0 − 0 ) )
250 0m0e0 ⊢ ( 0 − 0 ) = 0
251 249 250 eqtrdi ⊢ ( 𝑘 = 0 → ( 0 − 𝑘 ) = 0 )
252 251 fveq2d ⊢ ( 𝑘 = 0 → ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) )
253 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) = ( 0 ↑ ( 𝑁 ‘ 1 ) ) )
254 2fveq3 ⊢ ( 𝑘 = 0 → ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) = ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) )
255 254 fveq1d ⊢ ( 𝑘 = 0 → ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) = ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) )
256 253 255 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) ) = ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) )
257 252 256 eqeq12d ⊢ ( 𝑘 = 0 → ( ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) ) ↔ ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) = ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) ) )
258 248 257 ralsn ⊢ ( ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) ) ↔ ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) = ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) )
259 247 258 bitrdi ⊢ ( 𝑧 = ∅ → ( ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) = ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) ) )
260 141 259 ralsn ⊢ ( ∀ 𝑧 ∈ { ∅ } ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) = ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) )
261 243 260 sylibr ⊢ ( 𝜑 → ∀ 𝑧 ∈ { ∅ } ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
262 nfv ⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) )
263 nfra1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) )
264 262 263 nfan ⊢ Ⅎ 𝑧 ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
265 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) )
266 nfra2w ⊢ Ⅎ 𝑘 ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) )
267 265 266 nfan ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
268 nfv ⊢ Ⅎ 𝑘 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) )
269 267 268 nfan ⊢ Ⅎ 𝑘 ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) )
270 eqid ⊢ ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) = ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 )
271 eqid ⊢ ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) = ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 )
272 eqid ⊢ ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) = ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) )
273 14 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝐼 ∈ Fin )
274 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑖 ⊆ 𝐼 )
275 273 274 ssfid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑖 ∈ Fin )
276 snfi ⊢ { 𝑚 } ∈ Fin
277 276 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → { 𝑚 } ∈ Fin )
278 275 277 unfid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( 𝑖 ∪ { 𝑚 } ) ∈ Fin )
279 15 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑅 ∈ IDomn )
280 40 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝐵 ∈ V )
281 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) )
282 278 280 281 elmaprd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑧 : ( 𝑖 ∪ { 𝑚 } ) ⟶ 𝐵 )
283 2fveq3 ⊢ ( 𝑛 = 𝑜 → ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) = ( 𝐴 ‘ ( 𝑧 ‘ 𝑜 ) ) )
284 283 oveq2d ⊢ ( 𝑛 = 𝑜 → ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) = ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑜 ) ) ) )
285 284 cbvmptv ⊢ ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) = ( 𝑜 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑜 ) ) ) )
286 285 oveq2i ⊢ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) = ( 𝑀 Σg ( 𝑜 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑜 ) ) ) ) )
287 fznn0sub2 ⊢ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) → ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) )
288 287 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) )
289 ssun2 ⊢ { 𝑚 } ⊆ ( 𝑖 ∪ { 𝑚 } )
290 vsnid ⊢ 𝑚 ∈ { 𝑚 }
291 289 290 sselii ⊢ 𝑚 ∈ ( 𝑖 ∪ { 𝑚 } )
292 291 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑚 ∈ ( 𝑖 ∪ { 𝑚 } ) )
293 eqid ⊢ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) = ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } )
294 fveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ‘ 𝑛 ) = ( 𝑦 ‘ 𝑛 ) )
295 294 fveq2d ⊢ ( 𝑧 = 𝑦 → ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) = ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) )
296 295 oveq2d ⊢ ( 𝑧 = 𝑦 → ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) = ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) )
297 296 mpteq2dv ⊢ ( 𝑧 = 𝑦 → ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) )
298 297 oveq2d ⊢ ( 𝑧 = 𝑦 → ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) = ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) )
299 298 fveq2d ⊢ ( 𝑧 = 𝑦 → ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) = ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) )
300 299 fveq1d ⊢ ( 𝑧 = 𝑦 → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) )
301 fveq2 ⊢ ( 𝑧 = 𝑦 → ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) = ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) )
302 301 oveq2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) )
303 300 302 eqeq12d ⊢ ( 𝑧 = 𝑦 → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) ) )
304 303 ralbidv ⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) ) )
305 304 cbvralvw ⊢ ( ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑦 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) )
306 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) )
307 306 eldifbd ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ¬ 𝑚 ∈ 𝑖 )
308 disjsn ⊢ ( ( 𝑖 ∩ { 𝑚 } ) = ∅ ↔ ¬ 𝑚 ∈ 𝑖 )
309 307 308 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑖 ∩ { 𝑚 } ) = ∅ )
310 undif5 ⊢ ( ( 𝑖 ∩ { 𝑚 } ) = ∅ → ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) = 𝑖 )
311 309 310 syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) = 𝑖 )
312 311 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → 𝑖 = ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) )
313 312 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝐵 ↑m 𝑖 ) = ( 𝐵 ↑m ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) )
314 oveq2 ⊢ ( 𝑘 = 𝑙 → ( ( ♯ ‘ 𝑖 ) − 𝑘 ) = ( ( ♯ ‘ 𝑖 ) − 𝑙 ) )
315 314 fveq2d ⊢ ( 𝑘 = 𝑙 → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑙 ) ) )
316 oveq1 ⊢ ( 𝑘 = 𝑙 → ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) = ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) )
317 2fveq3 ⊢ ( 𝑘 = 𝑙 → ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) = ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) )
318 317 fveq1d ⊢ ( 𝑘 = 𝑙 → ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) = ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) )
319 316 318 oveq12d ⊢ ( 𝑘 = 𝑙 → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) )
320 315 319 eqeq12d ⊢ ( 𝑘 = 𝑙 → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) ↔ ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ) )
321 320 cbvralvw ⊢ ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) ↔ ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) )
322 312 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ♯ ‘ 𝑖 ) = ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) )
323 322 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 0 ... ( ♯ ‘ 𝑖 ) ) = ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) )
324 2fveq3 ⊢ ( 𝑛 = 𝑜 → ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) = ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) )
325 324 oveq2d ⊢ ( 𝑛 = 𝑜 → ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) = ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) )
326 325 cbvmptv ⊢ ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) = ( 𝑜 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) )
327 312 mpteq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑜 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) = ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) )
328 326 327 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) = ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) )
329 328 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) = ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) )
330 329 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) = ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) )
331 322 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( ♯ ‘ 𝑖 ) − 𝑙 ) = ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) )
332 330 331 fveq12d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑙 ) ) = ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) )
333 312 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑖 eval 𝑅 ) = ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) )
334 312 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑖 eSymPoly 𝑅 ) = ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) )
335 334 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) = ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) )
336 333 335 fveq12d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) = ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) )
337 336 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) = ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) )
338 337 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) )
339 332 338 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ↔ ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ) )
340 323 339 raleqbidv ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ↔ ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ) )
341 321 340 bitrid ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) ↔ ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ) )
342 313 341 raleqbidv ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ∀ 𝑦 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 𝐵 ↑m ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ) )
343 305 342 bitrid ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑦 ∈ ( 𝐵 ↑m ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ) )
344 343 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) → ∀ 𝑦 ∈ ( 𝐵 ↑m ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) )
345 344 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ∀ 𝑦 ∈ ( 𝐵 ↑m ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) )
346 eqid ⊢ ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) = ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 )
347 eqid ⊢ ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) = ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 )
348 eqid ⊢ ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) = ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) )
349 difssd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ⊆ ( 𝑖 ∪ { 𝑚 } ) )
350 278 349 ssfid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ∈ Fin )
351 282 349 fssresd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( 𝑧 ↾ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) : ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ⟶ 𝐵 )
352 eqid ⊢ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( ( 𝑧 ↾ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ‘ 𝑜 ) ) ) ) ) = ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( ( 𝑧 ↾ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ‘ 𝑜 ) ) ) ) )
353 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
354 1 2 3 4 346 347 7 8 9 10 11 12 348 350 279 351 352 353 vietadeg1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( ( 𝑧 ↾ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ‘ 𝑜 ) ) ) ) ) ) = ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) )
355 1 2 3 4 270 271 7 8 9 10 11 12 272 278 279 282 286 288 292 293 345 354 vietalem ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ) ) ‘ 𝑧 ) ) )
356 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → 𝐼 ∈ Fin )
357 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → 𝑖 ⊆ 𝐼 )
358 356 357 ssfid ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → 𝑖 ∈ Fin )
359 276 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → { 𝑚 } ∈ Fin )
360 358 359 unfid ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑖 ∪ { 𝑚 } ) ∈ Fin )
361 360 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( 𝑖 ∪ { 𝑚 } ) ∈ Fin )
362 hashcl ⊢ ( ( 𝑖 ∪ { 𝑚 } ) ∈ Fin → ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ∈ ℕ0 )
363 361 362 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ∈ ℕ0 )
364 363 nn0cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ∈ ℂ )
365 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) → 𝑘 ∈ ℕ0 )
366 365 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑘 ∈ ℕ0 )
367 366 nn0cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑘 ∈ ℂ )
368 364 367 nncand ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = 𝑘 )
369 368 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ↑ ( 𝑁 ‘ 1 ) ) = ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) )
370 368 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ) = ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) )
371 370 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ) ) = ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) )
372 371 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ) ) ‘ 𝑧 ) = ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) )
373 369 372 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
374 373 ad4ant14 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
375 355 374 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
376 269 375 ralrimia ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) → ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
377 264 376 ralrimia ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) → ∀ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
378 377 ex ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) → ∀ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
379 378 anasss ⊢ ( ( 𝜑 ∧ ( 𝑖 ⊆ 𝐼 ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ) → ( ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) → ∀ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
380 71 88 105 125 261 379 14 findcard2d ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝐵 ↑m 𝐼 ) ∀ 𝑘 ∈ ( 0 ... 𝐻 ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( 𝐻 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
381 40 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
382 381 14 16 elmapdd ⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ↑m 𝐼 ) )
383 31 38 380 382 18 rspc2dv ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐻 − 𝐾 ) ) = ( ( 𝐾 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝐾 ) ) ‘ 𝑍 ) ) )