Metamath Proof Explorer

Theorem coelem

Description: Lemma for properties of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion coelem 
|- ( F e. ( Poly ` S ) -> ( ( coeff ` F ) e. ( CC ^m NN0 ) /\ E. n e. NN0 ( ( ( coeff ` F ) " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 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 ) ) ) ) ) )
2 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 ) ) ) ) )
3 riotacl2 
 |-  ( 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 ) ) ) ) -> ( 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 ) ) ) ) ) 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 ) ) ) ) } )
4 2 3 syl 
 |-  ( F e. ( Poly ` S ) -> ( 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 ) ) ) ) ) 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 ) ) ) ) } )
5 1 4 eqeltrd 
 |-  ( F e. ( Poly ` S ) -> ( coeff ` F ) 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 ) ) ) ) } )
6 imaeq1 
 |-  ( a = ( coeff ` F ) -> ( a " ( ZZ>= ` ( n + 1 ) ) ) = ( ( coeff ` F ) " ( ZZ>= ` ( n + 1 ) ) ) )
7 6 eqeq1d 
 |-  ( a = ( coeff ` F ) -> ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } <-> ( ( coeff ` F ) " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } ) )
8 fveq1 
 |-  ( a = ( coeff ` F ) -> ( a ` k ) = ( ( coeff ` F ) ` k ) )
9 8 oveq1d 
 |-  ( a = ( coeff ` F ) -> ( ( a ` k ) x. ( z ^ k ) ) = ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) )
10 9 sumeq2sdv 
 |-  ( a = ( coeff ` F ) -> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... n ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) )
11 10 mpteq2dv 
 |-  ( a = ( coeff ` F ) -> ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) ) )
12 11 eqeq2d 
 |-  ( a = ( coeff ` F ) -> ( F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) <-> F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) ) ) )
13 7 12 anbi12d 
 |-  ( a = ( coeff ` F ) -> ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) <-> ( ( ( coeff ` F ) " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) ) ) ) )
14 13 rexbidv 
 |-  ( a = ( coeff ` F ) -> ( 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 ( ( ( coeff ` F ) " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) ) ) ) )
15 14 elrab 
 |-  ( ( coeff ` F ) 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 ) ) ) ) } <-> ( ( coeff ` F ) e. ( CC ^m NN0 ) /\ E. n e. NN0 ( ( ( coeff ` F ) " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) ) ) ) )
16 5 15 sylib 
 |-  ( F e. ( Poly ` S ) -> ( ( coeff ` F ) e. ( CC ^m NN0 ) /\ E. n e. NN0 ( ( ( coeff ` F ) " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) ) ) ) )