Metamath Proof Explorer

Theorem coe1fv

Description: Value of an evaluated coefficient in a polynomial coefficient vector. (Contributed by Stefan O'Rear, 21-Mar-2015)

Ref Expression
Hypothesis coe1fval.a 
|- A = ( coe1 ` F )
Assertion coe1fv 
|- ( ( F e. V /\ N e. NN0 ) -> ( A ` N ) = ( F ` ( 1o X. { N } ) ) )

Proof

Step Hyp Ref Expression
1 coe1fval.a 
 |-  A = ( coe1 ` F )
2 1 coe1fval 
 |-  ( F e. V -> A = ( n e. NN0 |-> ( F ` ( 1o X. { n } ) ) ) )
3 2 fveq1d 
 |-  ( F e. V -> ( A ` N ) = ( ( n e. NN0 |-> ( F ` ( 1o X. { n } ) ) ) ` N ) )
4 sneq 
 |-  ( n = N -> { n } = { N } )
5 4 xpeq2d 
 |-  ( n = N -> ( 1o X. { n } ) = ( 1o X. { N } ) )
6 5 fveq2d 
 |-  ( n = N -> ( F ` ( 1o X. { n } ) ) = ( F ` ( 1o X. { N } ) ) )
7 eqid 
 |-  ( n e. NN0 |-> ( F ` ( 1o X. { n } ) ) ) = ( n e. NN0 |-> ( F ` ( 1o X. { n } ) ) )
8 fvex 
 |-  ( F ` ( 1o X. { N } ) ) e. _V
9 6 7 8 fvmpt 
 |-  ( N e. NN0 -> ( ( n e. NN0 |-> ( F ` ( 1o X. { n } ) ) ) ` N ) = ( F ` ( 1o X. { N } ) ) )
10 3 9 sylan9eq 
 |-  ( ( F e. V /\ N e. NN0 ) -> ( A ` N ) = ( F ` ( 1o X. { N } ) ) )