Description: Define a function which maps a coefficient function for a univariate polynomial to the corresponding polynomial object. (Contributed by Mario Carneiro, 12-Jun-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-toply1 | |- toPoly1 = ( f e. _V |-> ( n e. ( NN0 ^m 1o ) |-> ( f ` ( n ` (/) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | ctp1 | |- toPoly1 |
|
| 1 | vf | |- f |
|
| 2 | cvv | |- _V |
|
| 3 | vn | |- n |
|
| 4 | cn0 | |- NN0 |
|
| 5 | cmap | |- ^m |
|
| 6 | c1o | |- 1o |
|
| 7 | 4 6 5 | co | |- ( NN0 ^m 1o ) |
| 8 | 1 | cv | |- f |
| 9 | 3 | cv | |- n |
| 10 | c0 | |- (/) |
|
| 11 | 10 9 | cfv | |- ( n ` (/) ) |
| 12 | 11 8 | cfv | |- ( f ` ( n ` (/) ) ) |
| 13 | 3 7 12 | cmpt | |- ( n e. ( NN0 ^m 1o ) |-> ( f ` ( n ` (/) ) ) ) |
| 14 | 1 2 13 | cmpt | |- ( f e. _V |-> ( n e. ( NN0 ^m 1o ) |-> ( f ` ( n ` (/) ) ) ) ) |
| 15 | 0 14 | wceq | |- toPoly1 = ( f e. _V |-> ( n e. ( NN0 ^m 1o ) |-> ( f ` ( n ` (/) ) ) ) ) |