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

Definition df-coe1 16573
Description: Define the coefficient function for a univariate polynomial. (Contributed by Stefan O'Rear, 21-Mar-2015.)
Assertion
Ref Expression
df-coe1  |- coe1  =  (
f  e.  _V  |->  ( n  e.  NN0  |->  ( f `
 ( 1o  X.  { n } ) ) ) )
Distinct variable group:    f, n

Detailed syntax breakdown of Definition df-coe1
StepHypRef Expression
1 cco1 16566 . 2  class coe1
2 vf . . 3  set  f
3 cvv 2948 . . 3  class  _V
4 vn . . . 4  set  n
5 cn0 10213 . . . 4  class  NN0
6 c1o 6709 . . . . . 6  class  1o
74cv 1651 . . . . . . 7  class  n
87csn 3806 . . . . . 6  class  { n }
96, 8cxp 4868 . . . . 5  class  ( 1o 
X.  { n }
)
102cv 1651 . . . . 5  class  f
119, 10cfv 5446 . . . 4  class  ( f `
 ( 1o  X.  { n } ) )
124, 5, 11cmpt 4258 . . 3  class  ( n  e.  NN0  |->  ( f `
 ( 1o  X.  { n } ) ) )
132, 3, 12cmpt 4258 . 2  class  ( f  e.  _V  |->  ( n  e.  NN0  |->  ( f `
 ( 1o  X.  { n } ) ) ) )
141, 13wceq 1652 1  wff coe1  =  (
f  e.  _V  |->  ( n  e.  NN0  |->  ( f `
 ( 1o  X.  { n } ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  coe1fval  16595
  Copyright terms: Public domain W3C validator