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 bilani ⊢ ( ( 𝜑 ∧ 𝑓 = ∅ ) → 𝑓 = ( ∅ × { 0 } ) )
151 150 iftrued ⊢ ( ( 𝜑 ∧ 𝑓 = ∅ ) → if ( 𝑓 = ( ∅ × { 0 } ) , 1 , ( 0g ‘ 𝑅 ) ) = 1 )
152 151 142 144 fmptsnd ⊢ ( 𝜑 → { ⟨ ∅ , 1 ⟩ } = ( 𝑓 ∈ { ∅ } ↦ if ( 𝑓 = ( ∅ × { 0 } ) , 1 , ( 0g ‘ 𝑅 ) ) ) )
153 140 146 152 3eqtrd ⊢ ( 𝜑 → ( { ∅ } × { ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) } ) = ( 𝑓 ∈ { ∅ } ↦ if ( 𝑓 = ( ∅ × { 0 } ) , 1 , ( 0g ‘ 𝑅 ) ) ) )
154 elsni ⊢ ( ℎ ∈ { ∅ } → ℎ = ∅ )
155 nn0ex ⊢ ℕ0 ∈ V
156 mapdm0 ⊢ ( ℕ0 ∈ V → ( ℕ0 ↑m ∅ ) = { ∅ } )
157 155 156 ax-mp ⊢ ( ℕ0 ↑m ∅ ) = { ∅ }
158 154 157 eleq2s ⊢ ( ℎ ∈ ( ℕ0 ↑m ∅ ) → ℎ = ∅ )
159 158 cnveqd ⊢ ( ℎ ∈ ( ℕ0 ↑m ∅ ) → ◡ ℎ = ◡ ∅ )
160 159 imaeq1d ⊢ ( ℎ ∈ ( ℕ0 ↑m ∅ ) → ( ◡ ℎ “ ℕ ) = ( ◡ ∅ “ ℕ ) )
161 cnv0 ⊢ ◡ ∅ = ∅
162 161 imaeq1i ⊢ ( ◡ ∅ “ ℕ ) = ( ∅ “ ℕ )
163 0ima ⊢ ( ∅ “ ℕ ) = ∅
164 162 163 eqtri ⊢ ( ◡ ∅ “ ℕ ) = ∅
165 160 164 eqtrdi ⊢ ( ℎ ∈ ( ℕ0 ↑m ∅ ) → ( ◡ ℎ “ ℕ ) = ∅ )
166 0fi ⊢ ∅ ∈ Fin
167 165 166 eqeltrdi ⊢ ( ℎ ∈ ( ℕ0 ↑m ∅ ) → ( ◡ ℎ “ ℕ ) ∈ Fin )
168 167 rabeqc ⊢ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = ( ℕ0 ↑m ∅ )
169 168 157 eqtr2i ⊢ { ∅ } = { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
170 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 }
171 170 psrbasfsupp ⊢ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
172 169 171 eqtr4i ⊢ { ∅ } = { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 }
173 0nn0 ⊢ 0 ∈ ℕ0
174 173 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
175 172 142 15 174 esplyfval ⊢ ( 𝜑 → ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ { ∅ } ) ‘ ( ( 𝟭 ‘ ∅ ) “ { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) ) )
176 fveqeq2 ⊢ ( 𝑐 = ∅ → ( ( ♯ ‘ 𝑐 ) = 0 ↔ ( ♯ ‘ ∅ ) = 0 ) )
177 0elpw ⊢ ∅ ∈ 𝒫 ∅
178 177 a1i ⊢ ( 𝜑 → ∅ ∈ 𝒫 ∅ )
179 46 a1i ⊢ ( 𝜑 → ( ♯ ‘ ∅ ) = 0 )
180 hasheq0 ⊢ ( 𝑐 ∈ 𝒫 ∅ → ( ( ♯ ‘ 𝑐 ) = 0 ↔ 𝑐 = ∅ ) )
181 180 biimpa ⊢ ( ( 𝑐 ∈ 𝒫 ∅ ∧ ( ♯ ‘ 𝑐 ) = 0 ) → 𝑐 = ∅ )
182 181 adantll ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 ∅ ) ∧ ( ♯ ‘ 𝑐 ) = 0 ) → 𝑐 = ∅ )
183 176 178 179 182 rabeqsnd ⊢ ( 𝜑 → { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } = { ∅ } )
184 183 imaeq2d ⊢ ( 𝜑 → ( ( 𝟭 ‘ ∅ ) “ { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } ) = ( ( 𝟭 ‘ ∅ ) “ { ∅ } ) )
185 pw0 ⊢ 𝒫 ∅ = { ∅ }
186 185 a1i ⊢ ( 𝜑 → 𝒫 ∅ = { ∅ } )
187 indf1o ⊢ ( ∅ ∈ V → ( 𝟭 ‘ ∅ ) : 𝒫 ∅ –1-1-onto→ ( { 0 , 1 } ↑m ∅ ) )
188 f1of ⊢ ( ( 𝟭 ‘ ∅ ) : 𝒫 ∅ –1-1-onto→ ( { 0 , 1 } ↑m ∅ ) → ( 𝟭 ‘ ∅ ) : 𝒫 ∅ ⟶ ( { 0 , 1 } ↑m ∅ ) )
189 142 187 188 3syl ⊢ ( 𝜑 → ( 𝟭 ‘ ∅ ) : 𝒫 ∅ ⟶ ( { 0 , 1 } ↑m ∅ ) )
190 186 189 feq2dd ⊢ ( 𝜑 → ( 𝟭 ‘ ∅ ) : { ∅ } ⟶ ( { 0 , 1 } ↑m ∅ ) )
191 190 ffnd ⊢ ( 𝜑 → ( 𝟭 ‘ ∅ ) Fn { ∅ } )
192 141 snid ⊢ ∅ ∈ { ∅ }
193 192 a1i ⊢ ( 𝜑 → ∅ ∈ { ∅ } )
194 191 193 fnimasnd ⊢ ( 𝜑 → ( ( 𝟭 ‘ ∅ ) “ { ∅ } ) = { ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) } )
195 ssidd ⊢ ( 𝜑 → ∅ ⊆ ∅ )
196 indf ⊢ ( ( ∅ ∈ V ∧ ∅ ⊆ ∅ ) → ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) : ∅ ⟶ { 0 , 1 } )
197 142 195 196 syl2anc ⊢ ( 𝜑 → ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) : ∅ ⟶ { 0 , 1 } )
198 f0bi ⊢ ( ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) : ∅ ⟶ { 0 , 1 } ↔ ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) = ∅ )
199 197 198 sylib ⊢ ( 𝜑 → ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) = ∅ )
200 199 sneqd ⊢ ( 𝜑 → { ( ( 𝟭 ‘ ∅ ) ‘ ∅ ) } = { ∅ } )
201 184 194 200 3eqtrd ⊢ ( 𝜑 → ( ( 𝟭 ‘ ∅ ) “ { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } ) = { ∅ } )
202 201 fveq2d ⊢ ( 𝜑 → ( ( 𝟭 ‘ { ∅ } ) ‘ ( ( 𝟭 ‘ ∅ ) “ { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) = ( ( 𝟭 ‘ { ∅ } ) ‘ { ∅ } ) )
203 p0ex ⊢ { ∅ } ∈ V
204 indconst1 ⊢ ( { ∅ } ∈ V → ( ( 𝟭 ‘ { ∅ } ) ‘ { ∅ } ) = ( { ∅ } × { 1 } ) )
205 203 204 ax-mp ⊢ ( ( 𝟭 ‘ { ∅ } ) ‘ { ∅ } ) = ( { ∅ } × { 1 } )
206 202 205 eqtrdi ⊢ ( 𝜑 → ( ( 𝟭 ‘ { ∅ } ) ‘ ( ( 𝟭 ‘ ∅ ) “ { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) = ( { ∅ } × { 1 } ) )
207 206 coeq2d ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ { ∅ } ) ‘ ( ( 𝟭 ‘ ∅ ) “ { 𝑐 ∈ 𝒫 ∅ ∣ ( ♯ ‘ 𝑐 ) = 0 } ) ) ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( { ∅ } × { 1 } ) ) )
208 136 zrhrhm ⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
209 zringbas ⊢ ℤ = ( Base ‘ ℤring )
210 209 2 rhmf ⊢ ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ 𝐵 )
211 126 208 210 3syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ 𝐵 )
212 211 ffnd ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) Fn ℤ )
213 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
214 fcoconst ⊢ ( ( ( ℤRHom ‘ 𝑅 ) Fn ℤ ∧ 1 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( { ∅ } × { 1 } ) ) = ( { ∅ } × { ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) } ) )
215 212 213 214 syl2anc ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( { ∅ } × { 1 } ) ) = ( { ∅ } × { ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) } ) )
216 175 207 215 3eqtrd ⊢ ( 𝜑 → ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) = ( { ∅ } × { ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) } ) )
217 eqid ⊢ ( ∅ mPoly 𝑅 ) = ( ∅ mPoly 𝑅 )
218 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
219 eqid ⊢ ( algSc ‘ ( ∅ mPoly 𝑅 ) ) = ( algSc ‘ ( ∅ mPoly 𝑅 ) )
220 217 169 218 2 219 142 126 127 mplascl ⊢ ( 𝜑 → ( ( algSc ‘ ( ∅ mPoly 𝑅 ) ) ‘ 1 ) = ( 𝑓 ∈ { ∅ } ↦ if ( 𝑓 = ( ∅ × { 0 } ) , 1 , ( 0g ‘ 𝑅 ) ) ) )
221 153 216 220 3eqtr4d ⊢ ( 𝜑 → ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) = ( ( algSc ‘ ( ∅ mPoly 𝑅 ) ) ‘ 1 ) )
222 221 fveq2d ⊢ ( 𝜑 → ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) = ( ( ∅ eval 𝑅 ) ‘ ( ( algSc ‘ ( ∅ mPoly 𝑅 ) ) ‘ 1 ) ) )
223 222 fveq1d ⊢ ( 𝜑 → ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) = ( ( ( ∅ eval 𝑅 ) ‘ ( ( algSc ‘ ( ∅ mPoly 𝑅 ) ) ‘ 1 ) ) ‘ ∅ ) )
224 eqid ⊢ ( ∅ eval 𝑅 ) = ( ∅ eval 𝑅 )
225 192 157 eleqtrri ⊢ ∅ ∈ ( ℕ0 ↑m ∅ )
226 225 a1i ⊢ ( 𝜑 → ∅ ∈ ( ℕ0 ↑m ∅ ) )
227 15 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
228 224 217 2 219 226 227 127 evlsca ⊢ ( 𝜑 → ( ( ∅ eval 𝑅 ) ‘ ( ( algSc ‘ ( ∅ mPoly 𝑅 ) ) ‘ 1 ) ) = ( ( 𝐵 ↑m ∅ ) × { 1 } ) )
229 228 fveq1d ⊢ ( 𝜑 → ( ( ( ∅ eval 𝑅 ) ‘ ( ( algSc ‘ ( ∅ mPoly 𝑅 ) ) ‘ 1 ) ) ‘ ∅ ) = ( ( ( 𝐵 ↑m ∅ ) × { 1 } ) ‘ ∅ ) )
230 192 42 eleqtrri ⊢ ∅ ∈ ( 𝐵 ↑m ∅ )
231 143 fvconst2 ⊢ ( ∅ ∈ ( 𝐵 ↑m ∅ ) → ( ( ( 𝐵 ↑m ∅ ) × { 1 } ) ‘ ∅ ) = 1 )
232 230 231 mp1i ⊢ ( 𝜑 → ( ( ( 𝐵 ↑m ∅ ) × { 1 } ) ‘ ∅ ) = 1 )
233 223 229 232 3eqtrd ⊢ ( 𝜑 → ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) = 1 )
234 135 233 oveq12d ⊢ ( 𝜑 → ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) = ( 1 · 1 ) )
235 iftrue ⊢ ( 𝑙 = 0 → if ( 𝑙 = 0 , 1 , ( 0g ‘ 𝑅 ) ) = 1 )
236 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
237 4 236 ringidval ⊢ ( 1r ‘ 𝑊 ) = ( 0g ‘ 𝑀 )
238 237 eqcomi ⊢ ( 0g ‘ 𝑀 ) = ( 1r ‘ 𝑊 )
239 1 238 218 8 coe1id ⊢ ( 𝑅 ∈ Ring → ( coe1 ‘ ( 0g ‘ 𝑀 ) ) = ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , 1 , ( 0g ‘ 𝑅 ) ) ) )
240 126 239 syl ⊢ ( 𝜑 → ( coe1 ‘ ( 0g ‘ 𝑀 ) ) = ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , 1 , ( 0g ‘ 𝑅 ) ) ) )
241 235 240 174 144 fvmptd4 ⊢ ( 𝜑 → ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) = 1 )
242 128 234 241 3eqtr4rd ⊢ ( 𝜑 → ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) = ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) )
243 fveq2 ⊢ ( 𝑧 = ∅ → ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) = ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) )
244 243 oveq2d ⊢ ( 𝑧 = ∅ → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) ) )
245 244 eqeq2d ⊢ ( 𝑧 = ∅ → ( ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) ) ) )
246 245 ralbidv ⊢ ( 𝑧 = ∅ → ( ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) ) ) )
247 c0ex ⊢ 0 ∈ V
248 oveq2 ⊢ ( 𝑘 = 0 → ( 0 − 𝑘 ) = ( 0 − 0 ) )
249 0m0e0 ⊢ ( 0 − 0 ) = 0
250 248 249 eqtrdi ⊢ ( 𝑘 = 0 → ( 0 − 𝑘 ) = 0 )
251 250 fveq2d ⊢ ( 𝑘 = 0 → ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) )
252 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) = ( 0 ↑ ( 𝑁 ‘ 1 ) ) )
253 2fveq3 ⊢ ( 𝑘 = 0 → ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) = ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) )
254 253 fveq1d ⊢ ( 𝑘 = 0 → ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) = ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) )
255 252 254 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) ) = ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) )
256 251 255 eqeq12d ⊢ ( 𝑘 = 0 → ( ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) ) ↔ ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) = ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) ) )
257 247 256 ralsn ⊢ ( ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ ∅ ) ) ↔ ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) = ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) )
258 246 257 bitrdi ⊢ ( 𝑧 = ∅ → ( ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) = ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) ) )
259 141 258 ralsn ⊢ ( ∀ 𝑧 ∈ { ∅ } ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ 0 ) = ( ( 0 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 0 ) ) ‘ ∅ ) ) )
260 242 259 sylibr ⊢ ( 𝜑 → ∀ 𝑧 ∈ { ∅ } ∀ 𝑘 ∈ { 0 } ( ( coe1 ‘ ( 0g ‘ 𝑀 ) ) ‘ ( 0 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ∅ eval 𝑅 ) ‘ ( ( ∅ eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
261 nfv ⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) )
262 nfra1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) )
263 261 262 nfan ⊢ Ⅎ 𝑧 ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
264 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) )
265 nfra2w ⊢ Ⅎ 𝑘 ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) )
266 264 265 nfan ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
267 nfv ⊢ Ⅎ 𝑘 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) )
268 266 267 nfan ⊢ Ⅎ 𝑘 ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) )
269 eqid ⊢ ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) = ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 )
270 eqid ⊢ ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) = ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 )
271 eqid ⊢ ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) = ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) )
272 14 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝐼 ∈ Fin )
273 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑖 ⊆ 𝐼 )
274 272 273 ssfid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑖 ∈ Fin )
275 snfi ⊢ { 𝑚 } ∈ Fin
276 275 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → { 𝑚 } ∈ Fin )
277 274 276 unfid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( 𝑖 ∪ { 𝑚 } ) ∈ Fin )
278 15 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑅 ∈ IDomn )
279 40 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝐵 ∈ V )
280 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) )
281 277 279 280 elmaprd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑧 : ( 𝑖 ∪ { 𝑚 } ) ⟶ 𝐵 )
282 2fveq3 ⊢ ( 𝑛 = 𝑜 → ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) = ( 𝐴 ‘ ( 𝑧 ‘ 𝑜 ) ) )
283 282 oveq2d ⊢ ( 𝑛 = 𝑜 → ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) = ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑜 ) ) ) )
284 283 cbvmptv ⊢ ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) = ( 𝑜 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑜 ) ) ) )
285 284 oveq2i ⊢ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) = ( 𝑀 Σg ( 𝑜 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑜 ) ) ) ) )
286 fznn0sub2 ⊢ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) → ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) )
287 286 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) )
288 ssun2 ⊢ { 𝑚 } ⊆ ( 𝑖 ∪ { 𝑚 } )
289 vsnid ⊢ 𝑚 ∈ { 𝑚 }
290 288 289 sselii ⊢ 𝑚 ∈ ( 𝑖 ∪ { 𝑚 } )
291 290 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑚 ∈ ( 𝑖 ∪ { 𝑚 } ) )
292 eqid ⊢ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) = ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } )
293 fveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ‘ 𝑛 ) = ( 𝑦 ‘ 𝑛 ) )
294 293 fveq2d ⊢ ( 𝑧 = 𝑦 → ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) = ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) )
295 294 oveq2d ⊢ ( 𝑧 = 𝑦 → ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) = ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) )
296 295 mpteq2dv ⊢ ( 𝑧 = 𝑦 → ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) )
297 296 oveq2d ⊢ ( 𝑧 = 𝑦 → ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) = ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) )
298 297 fveq2d ⊢ ( 𝑧 = 𝑦 → ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) = ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) )
299 298 fveq1d ⊢ ( 𝑧 = 𝑦 → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) )
300 fveq2 ⊢ ( 𝑧 = 𝑦 → ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) = ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) )
301 300 oveq2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) )
302 299 301 eqeq12d ⊢ ( 𝑧 = 𝑦 → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) ) )
303 302 ralbidv ⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) ) )
304 303 cbvralvw ⊢ ( ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑦 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) )
305 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) )
306 305 eldifbd ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ¬ 𝑚 ∈ 𝑖 )
307 disjsn ⊢ ( ( 𝑖 ∩ { 𝑚 } ) = ∅ ↔ ¬ 𝑚 ∈ 𝑖 )
308 306 307 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑖 ∩ { 𝑚 } ) = ∅ )
309 undif5 ⊢ ( ( 𝑖 ∩ { 𝑚 } ) = ∅ → ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) = 𝑖 )
310 308 309 syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) = 𝑖 )
311 310 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → 𝑖 = ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) )
312 311 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝐵 ↑m 𝑖 ) = ( 𝐵 ↑m ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) )
313 oveq2 ⊢ ( 𝑘 = 𝑙 → ( ( ♯ ‘ 𝑖 ) − 𝑘 ) = ( ( ♯ ‘ 𝑖 ) − 𝑙 ) )
314 313 fveq2d ⊢ ( 𝑘 = 𝑙 → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑙 ) ) )
315 oveq1 ⊢ ( 𝑘 = 𝑙 → ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) = ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) )
316 2fveq3 ⊢ ( 𝑘 = 𝑙 → ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) = ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) )
317 316 fveq1d ⊢ ( 𝑘 = 𝑙 → ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) = ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) )
318 315 317 oveq12d ⊢ ( 𝑘 = 𝑙 → ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) )
319 314 318 eqeq12d ⊢ ( 𝑘 = 𝑙 → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) ↔ ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ) )
320 319 cbvralvw ⊢ ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) ↔ ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) )
321 311 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ♯ ‘ 𝑖 ) = ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) )
322 321 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 0 ... ( ♯ ‘ 𝑖 ) ) = ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) )
323 2fveq3 ⊢ ( 𝑛 = 𝑜 → ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) = ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) )
324 323 oveq2d ⊢ ( 𝑛 = 𝑜 → ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) = ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) )
325 324 cbvmptv ⊢ ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) = ( 𝑜 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) )
326 311 mpteq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑜 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) = ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) )
327 325 326 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) = ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) )
328 327 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) = ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) )
329 328 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) = ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) )
330 321 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( ♯ ‘ 𝑖 ) − 𝑙 ) = ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) )
331 329 330 fveq12d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑙 ) ) = ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) )
332 311 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑖 eval 𝑅 ) = ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) )
333 311 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑖 eSymPoly 𝑅 ) = ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) )
334 333 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) = ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) )
335 332 334 fveq12d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) = ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) )
336 335 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) = ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) )
337 336 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) )
338 331 337 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ↔ ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ) )
339 322 338 raleqbidv ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ↔ ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ) )
340 320 339 bitrid ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) ↔ ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ) )
341 312 340 raleqbidv ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ∀ 𝑦 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 𝐵 ↑m ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ) )
342 304 341 bitrid ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑦 ∈ ( 𝐵 ↑m ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) ) )
343 342 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) → ∀ 𝑦 ∈ ( 𝐵 ↑m ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) )
344 343 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ∀ 𝑦 ∈ ( 𝐵 ↑m ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ∀ 𝑙 ∈ ( 0 ... ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑦 ‘ 𝑜 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) − 𝑙 ) ) = ( ( 𝑙 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑙 ) ) ‘ 𝑦 ) ) )
345 eqid ⊢ ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 ) = ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eval 𝑅 )
346 eqid ⊢ ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 ) = ( ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) eSymPoly 𝑅 )
347 eqid ⊢ ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) = ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) )
348 difssd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ⊆ ( 𝑖 ∪ { 𝑚 } ) )
349 277 348 ssfid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ∈ Fin )
350 281 348 fssresd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( 𝑧 ↾ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) : ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ⟶ 𝐵 )
351 eqid ⊢ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( ( 𝑧 ↾ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ‘ 𝑜 ) ) ) ) ) = ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( ( 𝑧 ↾ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ‘ 𝑜 ) ) ) ) )
352 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
353 1 2 3 4 345 346 7 8 9 10 11 12 347 349 278 350 351 352 vietadeg1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑀 Σg ( 𝑜 ∈ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( ( 𝑧 ↾ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) ‘ 𝑜 ) ) ) ) ) ) = ( ♯ ‘ ( ( 𝑖 ∪ { 𝑚 } ) ∖ { 𝑚 } ) ) )
354 1 2 3 4 269 270 7 8 9 10 11 12 271 277 278 281 285 287 291 292 344 353 vietalem ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ) ) ‘ 𝑧 ) ) )
355 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → 𝐼 ∈ Fin )
356 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → 𝑖 ⊆ 𝐼 )
357 355 356 ssfid ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → 𝑖 ∈ Fin )
358 275 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → { 𝑚 } ∈ Fin )
359 357 358 unfid ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( 𝑖 ∪ { 𝑚 } ) ∈ Fin )
360 359 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( 𝑖 ∪ { 𝑚 } ) ∈ Fin )
361 hashcl ⊢ ( ( 𝑖 ∪ { 𝑚 } ) ∈ Fin → ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ∈ ℕ0 )
362 360 361 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ∈ ℕ0 )
363 362 nn0cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ∈ ℂ )
364 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) → 𝑘 ∈ ℕ0 )
365 364 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑘 ∈ ℕ0 )
366 365 nn0cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → 𝑘 ∈ ℂ )
367 363 366 nncand ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = 𝑘 )
368 367 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ↑ ( 𝑁 ‘ 1 ) ) = ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) )
369 367 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ) = ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) )
370 369 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ) ) = ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) )
371 370 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ) ) ‘ 𝑧 ) = ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) )
372 368 371 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
373 372 ad4ant14 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) ) ) ‘ 𝑧 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
374 354 373 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ) → ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
375 268 374 ralrimia ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ) → ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
376 263 375 ralrimia ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ∧ ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) → ∀ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
377 376 ex ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐼 ) ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) → ( ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) → ∀ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
378 377 anasss ⊢ ( ( 𝜑 ∧ ( 𝑖 ⊆ 𝐼 ∧ 𝑚 ∈ ( 𝐼 ∖ 𝑖 ) ) ) → ( ∀ 𝑧 ∈ ( 𝐵 ↑m 𝑖 ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑖 ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝑖 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ 𝑖 ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( 𝑖 eval 𝑅 ) ‘ ( ( 𝑖 eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) → ∀ 𝑧 ∈ ( 𝐵 ↑m ( 𝑖 ∪ { 𝑚 } ) ) ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ ( 𝑖 ∪ { 𝑚 } ) ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( ( ♯ ‘ ( 𝑖 ∪ { 𝑚 } ) ) − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( ( ( 𝑖 ∪ { 𝑚 } ) eval 𝑅 ) ‘ ( ( ( 𝑖 ∪ { 𝑚 } ) eSymPoly 𝑅 ) ‘ 𝑘 ) ) ‘ 𝑧 ) ) ) )
379 71 88 105 125 260 378 14 findcard2d ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝐵 ↑m 𝐼 ) ∀ 𝑘 ∈ ( 0 ... 𝐻 ) ( ( coe1 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑧 ‘ 𝑛 ) ) ) ) ) ) ‘ ( 𝐻 − 𝑘 ) ) = ( ( 𝑘 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝑘 ) ) ‘ 𝑧 ) ) )
380 40 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
381 380 14 16 elmapdd ⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ↑m 𝐼 ) )
382 31 38 379 381 18 rspc2dv ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐻 − 𝐾 ) ) = ( ( 𝐾 ↑ ( 𝑁 ‘ 1 ) ) · ( ( 𝑄 ‘ ( 𝐸 ‘ 𝐾 ) ) ‘ 𝑍 ) ) )