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

Definition df-toply1 16263
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 16256 . 2  class toPoly1
2 vf . . 3  set  f
3 cvv 2788 . . 3  class  _V
4 vn . . . 4  set  n
5 cn0 9965 . . . . 5  class  NN0
6 c1o 6472 . . . . 5  class  1o
7 cmap 6772 . . . . 5  class  ^m
85, 6, 7co 5858 . . . 4  class  ( NN0 
^m  1o )
9 c0 3455 . . . . . 6  class  (/)
104cv 1622 . . . . . 6  class  n
119, 10cfv 5255 . . . . 5  class  ( n `
 (/) )
122cv 1622 . . . . 5  class  f
1311, 12cfv 5255 . . . 4  class  ( f `
 ( n `  (/) ) )
144, 8, 13cmpt 4077 . . 3  class  ( n  e.  ( NN0  ^m  1o )  |->  ( f `
 ( n `  (/) ) ) )
152, 3, 14cmpt 4077 . 2  class  ( f  e.  _V  |->  ( n  e.  ( NN0  ^m  1o )  |->  ( f `
 ( n `  (/) ) ) ) )
161, 15wceq 1623 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