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

Definition df-coe1 19374
 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 19369 . 2 class coe1
2 vf . . 3 setvar 𝑓
3 cvv 3173 . . 3 class V
4 vn . . . 4 setvar 𝑛
5 cn0 11169 . . . 4 class 0
6 c1o 7440 . . . . . 6 class 1𝑜
74cv 1474 . . . . . . 7 class 𝑛
87csn 4125 . . . . . 6 class {𝑛}
96, 8cxp 5036 . . . . 5 class (1𝑜 × {𝑛})
102cv 1474 . . . . 5 class 𝑓
119, 10cfv 5804 . . . 4 class (𝑓‘(1𝑜 × {𝑛}))
124, 5, 11cmpt 4643 . . 3 class (𝑛 ∈ ℕ0 ↦ (𝑓‘(1𝑜 × {𝑛})))
132, 3, 12cmpt 4643 . 2 class (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1𝑜 × {𝑛}))))
141, 13wceq 1475 1 wff coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1𝑜 × {𝑛}))))
 Colors of variables: wff setvar class This definition is referenced by:  coe1fval  19396
 Copyright terms: Public domain W3C validator