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 20821
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 20816 . 2 class coe1
2 vf . . 3 setvar 𝑓
3 cvv 3480 . . 3 class V
4 vn . . . 4 setvar 𝑛
5 cn0 11896 . . . 4 class 0
6 c1o 8093 . . . . . 6 class 1o
74cv 1537 . . . . . . 7 class 𝑛
87csn 4550 . . . . . 6 class {𝑛}
96, 8cxp 5541 . . . . 5 class (1o × {𝑛})
102cv 1537 . . . . 5 class 𝑓
119, 10cfv 6345 . . . 4 class (𝑓‘(1o × {𝑛}))
124, 5, 11cmpt 5133 . . 3 class (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛})))
132, 3, 12cmpt 5133 . 2 class (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛}))))
141, 13wceq 1538 1 wff coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛}))))
Colors of variables: wff setvar class
This definition is referenced by:  coe1fval  20843
  Copyright terms: Public domain W3C validator