Metamath Proof Explorer

Theorem coe1f2

Description: Functionality of univariate power series coefficient vectors. (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 )
coe1f2.k 
|- K = ( Base ` R )
Assertion coe1f2 
|- ( F e. B -> A : NN0 --> K )

Proof

Step Hyp Ref Expression
1 coe1fval.a 
 |-  A = ( coe1 ` F )
2 coe1f2.b 
 |-  B = ( Base ` P )
3 coe1f2.p 
 |-  P = ( PwSer1 ` R )
4 coe1f2.k 
 |-  K = ( Base ` R )
5 3 2 4 psr1basf 
 |-  ( F e. B -> F : ( NN0 ^m 1o ) --> K )
6 df1o2 
 |-  1o = { (/) }
7 nn0ex 
 |-  NN0 e. _V
8 0ex 
 |-  (/) e. _V
9 eqid 
 |-  ( x e. NN0 |-> ( 1o X. { x } ) ) = ( x e. NN0 |-> ( 1o X. { x } ) )
10 6 7 8 9 mapsnf1o3 
 |-  ( x e. NN0 |-> ( 1o X. { x } ) ) : NN0 -1-1-onto-> ( NN0 ^m 1o )
11 f1of 
 |-  ( ( x e. NN0 |-> ( 1o X. { x } ) ) : NN0 -1-1-onto-> ( NN0 ^m 1o ) -> ( x e. NN0 |-> ( 1o X. { x } ) ) : NN0 --> ( NN0 ^m 1o ) )
12 10 11 ax-mp 
 |-  ( x e. NN0 |-> ( 1o X. { x } ) ) : NN0 --> ( NN0 ^m 1o )
13 fco 
 |-  ( ( F : ( NN0 ^m 1o ) --> K /\ ( x e. NN0 |-> ( 1o X. { x } ) ) : NN0 --> ( NN0 ^m 1o ) ) -> ( F o. ( x e. NN0 |-> ( 1o X. { x } ) ) ) : NN0 --> K )
14 5 12 13 sylancl 
 |-  ( F e. B -> ( F o. ( x e. NN0 |-> ( 1o X. { x } ) ) ) : NN0 --> K )
15 1 2 3 9 coe1fval3 
 |-  ( F e. B -> A = ( F o. ( x e. NN0 |-> ( 1o X. { x } ) ) ) )
16 15 feq1d 
 |-  ( F e. B -> ( A : NN0 --> K <-> ( F o. ( x e. NN0 |-> ( 1o X. { x } ) ) ) : NN0 --> K ) )
17 14 16 mpbird 
 |-  ( F e. B -> A : NN0 --> K )