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
|- A = ( coeff ` F )
dgrub.2
|- N = ( deg ` F )
Assertion coeid
|- ( F e. ( Poly ` S ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )

Proof

Step Hyp Ref Expression
1 dgrub.1
 |-  A = ( coeff ` F )
2 dgrub.2
 |-  N = ( deg ` F )
3 elply2
 |-  ( F e. ( Poly ` S ) <-> ( S C_ CC /\ E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( x e. CC |-> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) ) ) ) )
4 3 simprbi
 |-  ( F e. ( Poly ` S ) -> E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( x e. CC |-> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) ) ) )
5 simpll
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( x e. CC |-> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) ) ) ) -> F e. ( Poly ` S ) )
6 simplrl
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( x e. CC |-> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) ) ) ) -> n e. NN0 )
7 simplrr
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( x e. CC |-> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) ) ) ) -> a e. ( ( S u. { 0 } ) ^m NN0 ) )
8 simprl
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( x e. CC |-> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) ) ) ) -> ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } )
9 simprr
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( x e. CC |-> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) ) ) ) -> F = ( x e. CC |-> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) ) )
10 fveq2
 |-  ( m = k -> ( a ` m ) = ( a ` k ) )
11 oveq2
 |-  ( m = k -> ( x ^ m ) = ( x ^ k ) )
12 10 11 oveq12d
 |-  ( m = k -> ( ( a ` m ) x. ( x ^ m ) ) = ( ( a ` k ) x. ( x ^ k ) ) )
13 12 cbvsumv
 |-  sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) = sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( x ^ k ) )
14 oveq1
 |-  ( x = z -> ( x ^ k ) = ( z ^ k ) )
15 14 oveq2d
 |-  ( x = z -> ( ( a ` k ) x. ( x ^ k ) ) = ( ( a ` k ) x. ( z ^ k ) ) )
16 15 sumeq2sdv
 |-  ( x = z -> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( x ^ k ) ) = sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
17 13 16 syl5eq
 |-  ( x = z -> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) = sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
18 17 cbvmptv
 |-  ( x e. CC |-> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
19 9 18 eqtrdi
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( x e. CC |-> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) ) ) ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
20 1 2 5 6 7 8 19 coeidlem
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( x e. CC |-> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) ) ) ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
21 20 ex
 |-  ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( x e. CC |-> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) ) ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ) )
22 21 rexlimdvva
 |-  ( F e. ( Poly ` S ) -> ( E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( x e. CC |-> sum_ m e. ( 0 ... n ) ( ( a ` m ) x. ( x ^ m ) ) ) ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ) )
23 4 22 mpd
 |-  ( F e. ( Poly ` S ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )