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

Definition df-coe1 20279
Description: Define the coefficient function for a univariate polynomial. (Contributed by Stefan O'Rear, 21-Mar-2015.)
Assertion
Ref Expression
df-coe1 coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛}))))
Distinct variable group:   𝑓,𝑛

Detailed syntax breakdown of Definition df-coe1
StepHypRef Expression
1 cco1 20274 . 2 class coe1
2 vf . . 3 setvar 𝑓
3 cvv 3492 . . 3 class V
4 vn . . . 4 setvar 𝑛
5 cn0 11885 . . . 4 class 0
6 c1o 8084 . . . . . 6 class 1o
74cv 1527 . . . . . . 7 class 𝑛
87csn 4557 . . . . . 6 class {𝑛}
96, 8cxp 5546 . . . . 5 class (1o × {𝑛})
102cv 1527 . . . . 5 class 𝑓
119, 10cfv 6348 . . . 4 class (𝑓‘(1o × {𝑛}))
124, 5, 11cmpt 5137 . . 3 class (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛})))
132, 3, 12cmpt 5137 . 2 class (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛}))))
141, 13wceq 1528 1 wff coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛}))))
Colors of variables: wff setvar class
This definition is referenced by:  coe1fval  20301
  Copyright terms: Public domain W3C validator