MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-toply1 Structured version   Unicode version

Definition df-toply1 18712
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.)
Assertion
Ref Expression
df-toply1  |- toPoly1  =  ( f  e.  _V  |->  ( n  e.  ( NN0  ^m  1o )  |->  ( f `  ( n `  (/) ) ) ) )
Distinct variable group:    f, n

Detailed syntax breakdown of Definition df-toply1
StepHypRef Expression
1 ctp1 18707 . 2  class toPoly1
2 vf . . 3  setvar  f
3 cvv 3087 . . 3  class  _V
4 vn . . . 4  setvar  n
5 cn0 10869 . . . . 5  class  NN0
6 c1o 7183 . . . . 5  class  1o
7 cmap 7480 . . . . 5  class  ^m
85, 6, 7co 6305 . . . 4  class  ( NN0 
^m  1o )
9 c0 3767 . . . . . 6  class  (/)
104cv 1436 . . . . . 6  class  n
119, 10cfv 5601 . . . . 5  class  ( n `
 (/) )
122cv 1436 . . . . 5  class  f
1311, 12cfv 5601 . . . 4  class  ( f `
 ( n `  (/) ) )
144, 8, 13cmpt 4484 . . 3  class  ( n  e.  ( NN0  ^m  1o )  |->  ( f `
 ( n `  (/) ) ) )
152, 3, 14cmpt 4484 . 2  class  ( f  e.  _V  |->  ( n  e.  ( NN0  ^m  1o )  |->  ( f `
 ( n `  (/) ) ) ) )
161, 15wceq 1437 1  wff toPoly1  =  ( f  e.  _V  |->  ( n  e.  ( NN0  ^m  1o )  |->  ( f `  ( n `  (/) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator