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 19481
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 19476 . 2 class coe1
2 vf . . 3 setvar 𝑓
3 cvv 3189 . . 3 class V
4 vn . . . 4 setvar 𝑛
5 cn0 11243 . . . 4 class 0
6 c1o 7505 . . . . . 6 class 1𝑜
74cv 1479 . . . . . . 7 class 𝑛
87csn 4153 . . . . . 6 class {𝑛}
96, 8cxp 5077 . . . . 5 class (1𝑜 × {𝑛})
102cv 1479 . . . . 5 class 𝑓
119, 10cfv 5852 . . . 4 class (𝑓‘(1𝑜 × {𝑛}))
124, 5, 11cmpt 4678 . . 3 class (𝑛 ∈ ℕ0 ↦ (𝑓‘(1𝑜 × {𝑛})))
132, 3, 12cmpt 4678 . 2 class (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1𝑜 × {𝑛}))))
141, 13wceq 1480 1 wff coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1𝑜 × {𝑛}))))
Colors of variables: wff setvar class
This definition is referenced by:  coe1fval  19503
  Copyright terms: Public domain W3C validator