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 19768
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 ↦ (𝑓‘(1𝑜 × {𝑛}))))
Distinct variable group:   𝑓,𝑛

Detailed syntax breakdown of Definition df-coe1
StepHypRef Expression
1 cco1 19763 . 2 class coe1
2 vf . . 3 setvar 𝑓
3 cvv 3351 . . 3 class V
4 vn . . . 4 setvar 𝑛
5 cn0 11494 . . . 4 class 0
6 c1o 7706 . . . . . 6 class 1𝑜
74cv 1630 . . . . . . 7 class 𝑛
87csn 4316 . . . . . 6 class {𝑛}
96, 8cxp 5247 . . . . 5 class (1𝑜 × {𝑛})
102cv 1630 . . . . 5 class 𝑓
119, 10cfv 6031 . . . 4 class (𝑓‘(1𝑜 × {𝑛}))
124, 5, 11cmpt 4863 . . 3 class (𝑛 ∈ ℕ0 ↦ (𝑓‘(1𝑜 × {𝑛})))
132, 3, 12cmpt 4863 . 2 class (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1𝑜 × {𝑛}))))
141, 13wceq 1631 1 wff coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1𝑜 × {𝑛}))))
Colors of variables: wff setvar class
This definition is referenced by:  coe1fval  19790
  Copyright terms: Public domain W3C validator