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

Definition df-coe1 16278
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 16271 . 2  class coe1
2 vf . . 3  set  f
3 cvv 2801 . . 3  class  _V
4 vn . . . 4  set  n
5 cn0 9981 . . . 4  class  NN0
6 c1o 6488 . . . . . 6  class  1o
74cv 1631 . . . . . . 7  class  n
87csn 3653 . . . . . 6  class  { n }
96, 8cxp 4703 . . . . 5  class  ( 1o 
X.  { n }
)
102cv 1631 . . . . 5  class  f
119, 10cfv 5271 . . . 4  class  ( f `
 ( 1o  X.  { n } ) )
124, 5, 11cmpt 4093 . . 3  class  ( n  e.  NN0  |->  ( f `
 ( 1o  X.  { n } ) ) )
132, 3, 12cmpt 4093 . 2  class  ( f  e.  _V  |->  ( n  e.  NN0  |->  ( f `
 ( 1o  X.  { n } ) ) ) )
141, 13wceq 1632 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  16302
  Copyright terms: Public domain W3C validator