Metamath Proof Explorer

Theorem coeid

Description: Reconstruct a polynomial as an explicit sum of the coefficient function up to the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses dgrub.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
dgrub.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
Assertion coeid ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 dgrub.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 dgrub.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
3 elply2 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) )
4 3 simprbi ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) )
5 simpll ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
6 simplrl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → 𝑛 ∈ ℕ0 )
7 simplrr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
8 simprl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } )
9 simprr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) )
10 fveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝑎 ‘ 𝑚 ) = ( 𝑎 ‘ 𝑘 ) )
11 oveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝑥 ↑ 𝑚 ) = ( 𝑥 ↑ 𝑘 ) )
12 10 11 oveq12d ⊢ ( 𝑚 = 𝑘 → ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) = ( ( 𝑎 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
13 12 cbvsumv ⊢ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) )
14 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ↑ 𝑘 ) = ( 𝑧 ↑ 𝑘 ) )
15 14 oveq2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) = ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
16 15 sumeq2sdv ⊢ ( 𝑥 = 𝑧 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
17 13 16 syl5eq ⊢ ( 𝑥 = 𝑧 → Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
18 17 cbvmptv ⊢ ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
19 9 18 syl6eq ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
20 1 2 5 6 7 8 19 coeidlem ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
21 20 ex ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
22 21 rexlimdvva ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
23 4 22 mpd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )