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 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑚 ) · ( 𝑥𝑚 ) ) ) ) ) )
4 3 simprbi ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑚 ) · ( 𝑥𝑚 ) ) ) ) )
5 simpll ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑚 ) · ( 𝑥𝑚 ) ) ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
6 simplrl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑚 ) · ( 𝑥𝑚 ) ) ) ) ) → 𝑛 ∈ ℕ0 )
7 simplrr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑚 ) · ( 𝑥𝑚 ) ) ) ) ) → 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) )
8 simprl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑚 ) · ( 𝑥𝑚 ) ) ) ) ) → ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } )
9 simprr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 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 eqtrdi ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑚 ) · ( 𝑥𝑚 ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) )
20 1 2 5 6 7 8 19 coeidlem ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑚 ) · ( 𝑥𝑚 ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ) )
21 20 ex ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) → ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑚 ) · ( 𝑥𝑚 ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
22 21 rexlimdvva ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑚 ) · ( 𝑥𝑚 ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
23 4 22 mpd ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ) )