Metamath Proof Explorer

Theorem coeeq

Description: If A satisfies the properties of the coefficient function, it must be equal to the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses coeeq.1 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
coeeq.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
coeeq.3 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
coeeq.4 ⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
coeeq.5 ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
Assertion coeeq ( 𝜑 → ( coeff ‘ 𝐹 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 coeeq.1 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
2 coeeq.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3 coeeq.3 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
4 coeeq.4 ⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
5 coeeq.5 ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
6 coeval ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) = ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
7 1 6 syl ⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) = ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
8 fvoveq1 ⊢ ( 𝑛 = 𝑁 → ( ℤ≥ ‘ ( 𝑛 + 1 ) ) = ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
9 8 imaeq2d ⊢ ( 𝑛 = 𝑁 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
10 9 eqeq1d ⊢ ( 𝑛 = 𝑁 → ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ) )
11 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 0 ... 𝑛 ) = ( 0 ... 𝑁 ) )
12 11 sumeq1d ⊢ ( 𝑛 = 𝑁 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
13 12 mpteq2dv ⊢ ( 𝑛 = 𝑁 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
14 13 eqeq2d ⊢ ( 𝑛 = 𝑁 → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
15 10 14 anbi12d ⊢ ( 𝑛 = 𝑁 → ( ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
16 15 rspcev ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → ∃ 𝑛 ∈ ℕ0 ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
17 2 4 5 16 syl12anc ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ0 ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
18 cnex ⊢ ℂ ∈ V
19 nn0ex ⊢ ℕ0 ∈ V
20 18 19 elmap ⊢ ( 𝐴 ∈ ( ℂ ↑m ℕ0 ) ↔ 𝐴 : ℕ0 ⟶ ℂ )
21 3 20 sylibr ⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ↑m ℕ0 ) )
22 coeeu ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃! 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
23 1 22 syl ⊢ ( 𝜑 → ∃! 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
24 imaeq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = ( 𝐴 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) )
25 24 eqeq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ) )
26 fveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
27 26 oveq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
28 27 sumeq2sdv ⊢ ( 𝑎 = 𝐴 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
29 28 mpteq2dv ⊢ ( 𝑎 = 𝐴 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
30 29 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
31 25 30 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
32 31 rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ0 ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
33 32 riota2 ⊢ ( ( 𝐴 ∈ ( ℂ ↑m ℕ0 ) ∧ ∃! 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → ( ∃ 𝑛 ∈ ℕ0 ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) = 𝐴 ) )
34 21 23 33 syl2anc ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ0 ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) = 𝐴 ) )
35 17 34 mpbid ⊢ ( 𝜑 → ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) = 𝐴 )
36 7 35 eqtrd ⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) = 𝐴 )