Metamath Proof Explorer

Theorem coe1fval

Description: Value of the univariate polynomial coefficient function. (Contributed by Stefan O'Rear, 21-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 coe1fval.a 
 |-  A = ( coe1 ` F )
2 elex 
 |-  ( F e. V -> F e. _V )
3 fveq1 
 |-  ( f = F -> ( f ` ( 1o X. { n } ) ) = ( F ` ( 1o X. { n } ) ) )
4 3 mpteq2dv 
 |-  ( f = F -> ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) ) = ( n e. NN0 |-> ( F ` ( 1o X. { n } ) ) ) )
5 df-coe1 
 |-  coe1 = ( f e. _V |-> ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) ) )
6 nn0ex 
 |-  NN0 e. _V
7 6 mptex 
 |-  ( n e. NN0 |-> ( F ` ( 1o X. { n } ) ) ) e. _V
8 4 5 7 fvmpt 
 |-  ( F e. _V -> ( coe1 ` F ) = ( n e. NN0 |-> ( F ` ( 1o X. { n } ) ) ) )
9 1 8 eqtrid 
 |-  ( F e. _V -> A = ( n e. NN0 |-> ( F ` ( 1o X. { n } ) ) ) )
10 2 9 syl 
 |-  ( F e. V -> A = ( n e. NN0 |-> ( F ` ( 1o X. { n } ) ) ) )