Metamath Proof Explorer

Theorem coeeq

Description: If A satisfies the properties of the coefficient function, it must be equal to the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses coeeq.1 
|- ( ph -> F e. ( Poly ` S ) )
coeeq.2 
|- ( ph -> N e. NN0 )
coeeq.3 
|- ( ph -> A : NN0 --> CC )
coeeq.4 
|- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
coeeq.5 
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
Assertion coeeq 
|- ( ph -> ( coeff ` F ) = A )

Proof

Step Hyp Ref Expression
1 coeeq.1 
 |-  ( ph -> F e. ( Poly ` S ) )
2 coeeq.2 
 |-  ( ph -> N e. NN0 )
3 coeeq.3 
 |-  ( ph -> A : NN0 --> CC )
4 coeeq.4 
 |-  ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
5 coeeq.5 
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
6 coeval 
 |-  ( F e. ( Poly ` S ) -> ( coeff ` F ) = ( iota_ a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) )
7 1 6 syl 
 |-  ( ph -> ( coeff ` F ) = ( iota_ a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) )
8 fvoveq1 
 |-  ( n = N -> ( ZZ>= ` ( n + 1 ) ) = ( ZZ>= ` ( N + 1 ) ) )
9 8 imaeq2d 
 |-  ( n = N -> ( A " ( ZZ>= ` ( n + 1 ) ) ) = ( A " ( ZZ>= ` ( N + 1 ) ) ) )
10 9 eqeq1d 
 |-  ( n = N -> ( ( A " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } <-> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) )
11 oveq2 
 |-  ( n = N -> ( 0 ... n ) = ( 0 ... N ) )
12 11 sumeq1d 
 |-  ( n = N -> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) )
13 12 mpteq2dv 
 |-  ( n = N -> ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
14 13 eqeq2d 
 |-  ( n = N -> ( F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( z ^ k ) ) ) <-> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ) )
15 10 14 anbi12d 
 |-  ( n = N -> ( ( ( A " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( z ^ k ) ) ) ) <-> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ) ) )
16 15 rspcev 
 |-  ( ( N e. NN0 /\ ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ) ) -> E. n e. NN0 ( ( A " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( z ^ k ) ) ) ) )
17 2 4 5 16 syl12anc 
 |-  ( ph -> E. n e. NN0 ( ( A " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( z ^ k ) ) ) ) )
18 cnex 
 |-  CC e. _V
19 nn0ex 
 |-  NN0 e. _V
20 18 19 elmap 
 |-  ( A e. ( CC ^m NN0 ) <-> A : NN0 --> CC )
21 3 20 sylibr 
 |-  ( ph -> A e. ( CC ^m NN0 ) )
22 coeeu 
 |-  ( F e. ( Poly ` S ) -> E! a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
23 1 22 syl 
 |-  ( ph -> E! a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
24 imaeq1 
 |-  ( a = A -> ( a " ( ZZ>= ` ( n + 1 ) ) ) = ( A " ( ZZ>= ` ( n + 1 ) ) ) )
25 24 eqeq1d 
 |-  ( a = A -> ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } <-> ( A " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } ) )
26 fveq1 
 |-  ( a = A -> ( a ` k ) = ( A ` k ) )
27 26 oveq1d 
 |-  ( a = A -> ( ( a ` k ) x. ( z ^ k ) ) = ( ( A ` k ) x. ( z ^ k ) ) )
28 27 sumeq2sdv 
 |-  ( a = A -> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( z ^ k ) ) )
29 28 mpteq2dv 
 |-  ( a = A -> ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( z ^ k ) ) ) )
30 29 eqeq2d 
 |-  ( a = A -> ( F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) <-> F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( z ^ k ) ) ) ) )
31 25 30 anbi12d 
 |-  ( a = A -> ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) <-> ( ( A " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( z ^ k ) ) ) ) ) )
32 31 rexbidv 
 |-  ( a = A -> ( E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) <-> E. n e. NN0 ( ( A " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( z ^ k ) ) ) ) ) )
33 32 riota2 
 |-  ( ( A e. ( CC ^m NN0 ) /\ E! a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> ( E. n e. NN0 ( ( A " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( z ^ k ) ) ) ) <-> ( iota_ a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) = A ) )
34 21 23 33 syl2anc 
 |-  ( ph -> ( E. n e. NN0 ( ( A " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( z ^ k ) ) ) ) <-> ( iota_ a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) = A ) )
35 17 34 mpbid 
 |-  ( ph -> ( iota_ a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) = A )
36 7 35 eqtrd 
 |-  ( ph -> ( coeff ` F ) = A )