Metamath Proof Explorer

Theorem fvcoe1

Description: Value of a multivariate coefficient in terms of the coefficient vector. (Contributed by Stefan O'Rear, 21-Mar-2015)

Ref Expression
Hypothesis coe1fval.a 
|- A = ( coe1 ` F )
Assertion fvcoe1 
|- ( ( F e. V /\ X e. ( NN0 ^m 1o ) ) -> ( F ` X ) = ( A ` ( X ` (/) ) ) )

Proof

Step Hyp Ref Expression
1 coe1fval.a 
 |-  A = ( coe1 ` F )
2 df1o2 
 |-  1o = { (/) }
3 nn0ex 
 |-  NN0 e. _V
4 0ex 
 |-  (/) e. _V
5 2 3 4 mapsnconst 
 |-  ( X e. ( NN0 ^m 1o ) -> X = ( 1o X. { ( X ` (/) ) } ) )
6 5 adantl 
 |-  ( ( F e. V /\ X e. ( NN0 ^m 1o ) ) -> X = ( 1o X. { ( X ` (/) ) } ) )
7 6 fveq2d 
 |-  ( ( F e. V /\ X e. ( NN0 ^m 1o ) ) -> ( F ` X ) = ( F ` ( 1o X. { ( X ` (/) ) } ) ) )
8 elmapi 
 |-  ( X e. ( NN0 ^m 1o ) -> X : 1o --> NN0 )
9 0lt1o 
 |-  (/) e. 1o
10 ffvelrn 
 |-  ( ( X : 1o --> NN0 /\ (/) e. 1o ) -> ( X ` (/) ) e. NN0 )
11 8 9 10 sylancl 
 |-  ( X e. ( NN0 ^m 1o ) -> ( X ` (/) ) e. NN0 )
12 1 coe1fv 
 |-  ( ( F e. V /\ ( X ` (/) ) e. NN0 ) -> ( A ` ( X ` (/) ) ) = ( F ` ( 1o X. { ( X ` (/) ) } ) ) )
13 11 12 sylan2 
 |-  ( ( F e. V /\ X e. ( NN0 ^m 1o ) ) -> ( A ` ( X ` (/) ) ) = ( F ` ( 1o X. { ( X ` (/) ) } ) ) )
14 7 13 eqtr4d 
 |-  ( ( F e. V /\ X e. ( NN0 ^m 1o ) ) -> ( F ` X ) = ( A ` ( X ` (/) ) ) )