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 eqtrid 
 |-  ( 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 ) ) ) )