Metamath Proof Explorer

Theorem coeid3

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

Ref Expression
Hypotheses dgrub.1 
|- A = ( coeff ` F )
dgrub.2 
|- N = ( deg ` F )
Assertion coeid3 
|- ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) -> ( F ` X ) = sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( X ^ k ) ) )

Proof

Step Hyp Ref Expression
1 dgrub.1 
 |-  A = ( coeff ` F )
2 dgrub.2 
 |-  N = ( deg ` F )
3 1 2 coeid2 
 |-  ( ( F e. ( Poly ` S ) /\ X e. CC ) -> ( F ` X ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( X ^ k ) ) )
4 3 3adant2 
 |-  ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) -> ( F ` X ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( X ^ k ) ) )
5 fzss2 
 |-  ( M e. ( ZZ>= ` N ) -> ( 0 ... N ) C_ ( 0 ... M ) )
6 5 3ad2ant2 
 |-  ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) -> ( 0 ... N ) C_ ( 0 ... M ) )
7 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
8 1 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
9 8 3ad2ant1 
 |-  ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) -> A : NN0 --> CC )
10 9 ffvelcdmda 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. NN0 ) -> ( A ` k ) e. CC )
11 expcl 
 |-  ( ( X e. CC /\ k e. NN0 ) -> ( X ^ k ) e. CC )
12 11 3ad2antl3 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. NN0 ) -> ( X ^ k ) e. CC )
13 10 12 mulcld 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. NN0 ) -> ( ( A ` k ) x. ( X ^ k ) ) e. CC )
14 7 13 sylan2 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( X ^ k ) ) e. CC )
15 eldifn 
 |-  ( k e. ( ( 0 ... M ) \ ( 0 ... N ) ) -> -. k e. ( 0 ... N ) )
16 15 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> -. k e. ( 0 ... N ) )
17 simpl1 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> F e. ( Poly ` S ) )
18 eldifi 
 |-  ( k e. ( ( 0 ... M ) \ ( 0 ... N ) ) -> k e. ( 0 ... M ) )
19 elfzuz 
 |-  ( k e. ( 0 ... M ) -> k e. ( ZZ>= ` 0 ) )
20 18 19 syl 
 |-  ( k e. ( ( 0 ... M ) \ ( 0 ... N ) ) -> k e. ( ZZ>= ` 0 ) )
21 20 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> k e. ( ZZ>= ` 0 ) )
22 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
23 21 22 eleqtrrdi 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> k e. NN0 )
24 1 2 dgrub 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 /\ ( A ` k ) =/= 0 ) -> k <_ N )
25 24 3expia 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k <_ N ) )
26 17 23 25 syl2anc 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( ( A ` k ) =/= 0 -> k <_ N ) )
27 simpl2 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> M e. ( ZZ>= ` N ) )
28 eluzel2 
 |-  ( M e. ( ZZ>= ` N ) -> N e. ZZ )
29 27 28 syl 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> N e. ZZ )
30 elfz5 
 |-  ( ( k e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( k e. ( 0 ... N ) <-> k <_ N ) )
31 21 29 30 syl2anc 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( k e. ( 0 ... N ) <-> k <_ N ) )
32 26 31 sylibrd 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( ( A ` k ) =/= 0 -> k e. ( 0 ... N ) ) )
33 32 necon1bd 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( -. k e. ( 0 ... N ) -> ( A ` k ) = 0 ) )
34 16 33 mpd 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( A ` k ) = 0 )
35 34 oveq1d 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( ( A ` k ) x. ( X ^ k ) ) = ( 0 x. ( X ^ k ) ) )
36 elfznn0 
 |-  ( k e. ( 0 ... M ) -> k e. NN0 )
37 18 36 syl 
 |-  ( k e. ( ( 0 ... M ) \ ( 0 ... N ) ) -> k e. NN0 )
38 37 12 sylan2 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( X ^ k ) e. CC )
39 38 mul02d 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( 0 x. ( X ^ k ) ) = 0 )
40 35 39 eqtrd 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( ( A ` k ) x. ( X ^ k ) ) = 0 )
41 fzfid 
 |-  ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) -> ( 0 ... M ) e. Fin )
42 6 14 40 41 fsumss 
 |-  ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) -> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( X ^ k ) ) = sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( X ^ k ) ) )
43 4 42 eqtrd 
 |-  ( ( F e. ( Poly ` S ) /\ M e. ( ZZ>= ` N ) /\ X e. CC ) -> ( F ` X ) = sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( X ^ k ) ) )