| 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 ) ) |