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

Definition df-coe1 17762
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 17757 . 2  class coe1
2 vf . . 3  setvar  f
3 cvv 3076 . . 3  class  _V
4 vn . . . 4  setvar  n
5 cn0 10689 . . . 4  class  NN0
6 c1o 7022 . . . . . 6  class  1o
74cv 1369 . . . . . . 7  class  n
87csn 3984 . . . . . 6  class  { n }
96, 8cxp 4945 . . . . 5  class  ( 1o 
X.  { n }
)
102cv 1369 . . . . 5  class  f
119, 10cfv 5525 . . . 4  class  ( f `
 ( 1o  X.  { n } ) )
124, 5, 11cmpt 4457 . . 3  class  ( n  e.  NN0  |->  ( f `
 ( 1o  X.  { n } ) ) )
132, 3, 12cmpt 4457 . 2  class  ( f  e.  _V  |->  ( n  e.  NN0  |->  ( f `
 ( 1o  X.  { n } ) ) ) )
141, 13wceq 1370 1  wff coe1  =  (
f  e.  _V  |->  ( n  e.  NN0  |->  ( f `
 ( 1o  X.  { n } ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  coe1fval  17784
  Copyright terms: Public domain W3C validator