Metamath Proof Explorer

Theorem coe1fval3

Description: Univariate power series coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypotheses coe1fval.a 
|- A = ( coe1 ` F )
coe1f2.b 
|- B = ( Base ` P )
coe1f2.p 
|- P = ( PwSer1 ` R )
coe1fval3.g 
|- G = ( y e. NN0 |-> ( 1o X. { y } ) )
Assertion coe1fval3 
|- ( F e. B -> A = ( F o. G ) )

Proof

Step Hyp Ref Expression
1 coe1fval.a 
 |-  A = ( coe1 ` F )
2 coe1f2.b 
 |-  B = ( Base ` P )
3 coe1f2.p 
 |-  P = ( PwSer1 ` R )
4 coe1fval3.g 
 |-  G = ( y e. NN0 |-> ( 1o X. { y } ) )
5 1 coe1fval 
 |-  ( F e. B -> A = ( y e. NN0 |-> ( F ` ( 1o X. { y } ) ) ) )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 3 2 6 psr1basf 
 |-  ( F e. B -> F : ( NN0 ^m 1o ) --> ( Base ` R ) )
8 ssv 
 |-  ( Base ` R ) C_ _V
9 fss 
 |-  ( ( F : ( NN0 ^m 1o ) --> ( Base ` R ) /\ ( Base ` R ) C_ _V ) -> F : ( NN0 ^m 1o ) --> _V )
10 7 8 9 sylancl 
 |-  ( F e. B -> F : ( NN0 ^m 1o ) --> _V )
11 fconst6g 
 |-  ( y e. NN0 -> ( 1o X. { y } ) : 1o --> NN0 )
12 11 adantl 
 |-  ( ( F : ( NN0 ^m 1o ) --> _V /\ y e. NN0 ) -> ( 1o X. { y } ) : 1o --> NN0 )
13 nn0ex 
 |-  NN0 e. _V
14 1oex 
 |-  1o e. _V
15 13 14 elmap 
 |-  ( ( 1o X. { y } ) e. ( NN0 ^m 1o ) <-> ( 1o X. { y } ) : 1o --> NN0 )
16 12 15 sylibr 
 |-  ( ( F : ( NN0 ^m 1o ) --> _V /\ y e. NN0 ) -> ( 1o X. { y } ) e. ( NN0 ^m 1o ) )
17 4 a1i 
 |-  ( F : ( NN0 ^m 1o ) --> _V -> G = ( y e. NN0 |-> ( 1o X. { y } ) ) )
18 id 
 |-  ( F : ( NN0 ^m 1o ) --> _V -> F : ( NN0 ^m 1o ) --> _V )
19 18 feqmptd 
 |-  ( F : ( NN0 ^m 1o ) --> _V -> F = ( x e. ( NN0 ^m 1o ) |-> ( F ` x ) ) )
20 fveq2 
 |-  ( x = ( 1o X. { y } ) -> ( F ` x ) = ( F ` ( 1o X. { y } ) ) )
21 16 17 19 20 fmptco 
 |-  ( F : ( NN0 ^m 1o ) --> _V -> ( F o. G ) = ( y e. NN0 |-> ( F ` ( 1o X. { y } ) ) ) )
22 10 21 syl 
 |-  ( F e. B -> ( F o. G ) = ( y e. NN0 |-> ( F ` ( 1o X. { y } ) ) ) )
23 5 22 eqtr4d 
 |-  ( F e. B -> A = ( F o. G ) )