Metamath Proof Explorer

Theorem elply2

Description: The coefficient function can be assumed to have zeroes outside 0 ... n . (Contributed by Mario Carneiro, 20-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion elply2 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elply ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
2 simpr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
3 simpll ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → 𝑆 ⊆ ℂ )
4 cnex ⊢ ℂ ∈ V
5 ssexg ⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑆 ∈ V )
6 3 4 5 sylancl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → 𝑆 ∈ V )
7 snex ⊢ { 0 } ∈ V
8 unexg ⊢ ( ( 𝑆 ∈ V ∧ { 0 } ∈ V ) → ( 𝑆 ∪ { 0 } ) ∈ V )
9 6 7 8 sylancl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ( 𝑆 ∪ { 0 } ) ∈ V )
10 nn0ex ⊢ ℕ0 ∈ V
11 elmapg ⊢ ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ ℕ0 ∈ V ) → ( 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝑓 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
12 9 10 11 sylancl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ( 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝑓 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
13 2 12 mpbid ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → 𝑓 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
14 13 ffvelcdmda ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑆 ∪ { 0 } ) )
15 ssun2 ⊢ { 0 } ⊆ ( 𝑆 ∪ { 0 } )
16 c0ex ⊢ 0 ∈ V
17 16 snss ⊢ ( 0 ∈ ( 𝑆 ∪ { 0 } ) ↔ { 0 } ⊆ ( 𝑆 ∪ { 0 } ) )
18 15 17 mpbir ⊢ 0 ∈ ( 𝑆 ∪ { 0 } )
19 ifcl ⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑆 ∪ { 0 } ) ∧ 0 ∈ ( 𝑆 ∪ { 0 } ) ) → if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ∈ ( 𝑆 ∪ { 0 } ) )
20 14 18 19 sylancl ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ 𝑥 ∈ ℕ0 ) → if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ∈ ( 𝑆 ∪ { 0 } ) )
21 20 fmpttd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
22 elmapg ⊢ ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ ℕ0 ∈ V ) → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
23 9 10 22 sylancl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
24 21 23 mpbird ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
25 eleq1w ⊢ ( 𝑥 = 𝑘 → ( 𝑥 ∈ ( 0 ... 𝑛 ) ↔ 𝑘 ∈ ( 0 ... 𝑛 ) ) )
26 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑘 ) )
27 25 26 ifbieq1d ⊢ ( 𝑥 = 𝑘 → if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) = if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑘 ) , 0 ) )
28 eqid ⊢ ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) )
29 fvex ⊢ ( 𝑓 ‘ 𝑘 ) ∈ V
30 29 16 ifex ⊢ if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑘 ) , 0 ) ∈ V
31 27 28 30 fvmpt ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑘 ) , 0 ) )
32 31 ad2antll ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ) → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑘 ) , 0 ) )
33 iffalse ⊢ ( ¬ 𝑘 ∈ ( 0 ... 𝑛 ) → if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑘 ) , 0 ) = 0 )
34 33 eqeq2d ⊢ ( ¬ 𝑘 ∈ ( 0 ... 𝑛 ) → ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑘 ) , 0 ) ↔ ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) = 0 ) )
35 32 34 syl5ibcom ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑛 ) → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) = 0 ) )
36 35 necon1ad ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ) → ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ ( 0 ... 𝑛 ) ) )
37 elfzle2 ⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → 𝑘 ≤ 𝑛 )
38 36 37 syl6 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ) → ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑛 ) )
39 38 anassrs ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑛 ) )
40 39 ralrimiva ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ∀ 𝑘 ∈ ℕ0 ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑛 ) )
41 simplr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → 𝑛 ∈ ℕ0 )
42 0cnd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → 0 ∈ ℂ )
43 42 snssd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → { 0 } ⊆ ℂ )
44 3 43 unssd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
45 21 44 fssd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) : ℕ0 ⟶ ℂ )
46 plyco0 ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) : ℕ0 ⟶ ℂ ) → ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑛 ) ) )
47 41 45 46 syl2anc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑛 ) ) )
48 40 47 mpbird ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } )
49 eqidd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
50 imaeq1 ⊢ ( 𝑎 = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) → ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) )
51 50 eqeq1d ⊢ ( 𝑎 = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) → ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ) )
52 fveq1 ⊢ ( 𝑎 = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) → ( 𝑎 ‘ 𝑘 ) = ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) )
53 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → 𝑘 ∈ ℕ0 )
54 53 31 syl ⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑘 ) , 0 ) )
55 iftrue ⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑘 ) , 0 ) = ( 𝑓 ‘ 𝑘 ) )
56 54 55 eqtrd ⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
57 52 56 sylan9eq ⊢ ( ( 𝑎 = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑎 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
58 57 oveq1d ⊢ ( ( 𝑎 = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
59 58 sumeq2dv ⊢ ( 𝑎 = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
60 59 mpteq2dv ⊢ ( 𝑎 = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
61 60 eqeq2d ⊢ ( 𝑎 = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
62 51 61 anbi12d ⊢ ( 𝑎 = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) → ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
63 62 rspcev ⊢ ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 ∈ ( 0 ... 𝑛 ) , ( 𝑓 ‘ 𝑥 ) , 0 ) ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
64 24 48 49 63 syl12anc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
65 eqeq1 ⊢ ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
66 65 anbi2d ⊢ ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
67 66 rexbidv ⊢ ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
68 64 67 syl5ibrcom ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
69 68 rexlimdva ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( ∃ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
70 69 reximdva ⊢ ( 𝑆 ⊆ ℂ → ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
71 70 imdistani ⊢ ( ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑓 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑓 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) → ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
72 1 71 sylbi ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
73 simpr ⊢ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
74 73 reximi ⊢ ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) → ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
75 74 reximi ⊢ ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) → ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
76 75 anim2i ⊢ ( ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
77 elply ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
78 76 77 sylibr ⊢ ( ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
79 72 78 impbii ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )