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 ‘ 𝐹 ) = ( 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
7 1 6 syl ( 𝜑 → ( coeff ‘ 𝐹 ) = ( 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ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 ( 𝐴 ∈ ( ℂ ↑m0 ) ↔ 𝐴 : ℕ0 ⟶ ℂ )
21 3 20 sylibr ( 𝜑𝐴 ∈ ( ℂ ↑m0 ) )
22 coeeu ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃! 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
23 1 22 syl ( 𝜑 → ∃! 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ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 ( ( 𝐴 ∈ ( ℂ ↑m0 ) ∧ ∃! 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( ∃ 𝑛 ∈ ℕ0 ( ( 𝐴 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ) ) ↔ ( 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) = 𝐴 ) )
34 21 23 33 syl2anc ( 𝜑 → ( ∃ 𝑛 ∈ ℕ0 ( ( 𝐴 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ) ) ↔ ( 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) = 𝐴 ) )
35 17 34 mpbid ( 𝜑 → ( 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) = 𝐴 )
36 7 35 eqtrd ( 𝜑 → ( coeff ‘ 𝐹 ) = 𝐴 )