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

Definition df-toply1 16545
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 16538 . 2  class toPoly1
2 vf . . 3  set  f
3 cvv 2924 . . 3  class  _V
4 vn . . . 4  set  n
5 cn0 10185 . . . . 5  class  NN0
6 c1o 6684 . . . . 5  class  1o
7 cmap 6985 . . . . 5  class  ^m
85, 6, 7co 6048 . . . 4  class  ( NN0 
^m  1o )
9 c0 3596 . . . . . 6  class  (/)
104cv 1648 . . . . . 6  class  n
119, 10cfv 5421 . . . . 5  class  ( n `
 (/) )
122cv 1648 . . . . 5  class  f
1311, 12cfv 5421 . . . 4  class  ( f `
 ( n `  (/) ) )
144, 8, 13cmpt 4234 . . 3  class  ( n  e.  ( NN0  ^m  1o )  |->  ( f `
 ( n `  (/) ) ) )
152, 3, 14cmpt 4234 . 2  class  ( f  e.  _V  |->  ( n  e.  ( NN0  ^m  1o )  |->  ( f `
 ( n `  (/) ) ) ) )
161, 15wceq 1649 1  wff toPoly1  =  ( f  e.  _V  |->  ( n  e.  ( NN0  ^m  1o )  |->  ( f `  ( n `  (/) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator