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

Definition df-toply1 19375
 Description: Define a function which maps a coefficient function for a univariate polynomial to the corresponding polynomial object. (Contributed by Mario Carneiro, 12-Jun-2015.)
Assertion
Ref Expression
df-toply1 toPoly1 = (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0𝑚 1𝑜) ↦ (𝑓‘(𝑛‘∅))))
Distinct variable group:   𝑓,𝑛

Detailed syntax breakdown of Definition df-toply1
StepHypRef Expression
1 ctp1 19370 . 2 class toPoly1
2 vf . . 3 setvar 𝑓
3 cvv 3173 . . 3 class V
4 vn . . . 4 setvar 𝑛
5 cn0 11169 . . . . 5 class 0
6 c1o 7440 . . . . 5 class 1𝑜
7 cmap 7744 . . . . 5 class 𝑚
85, 6, 7co 6549 . . . 4 class (ℕ0𝑚 1𝑜)
9 c0 3874 . . . . . 6 class
104cv 1474 . . . . . 6 class 𝑛
119, 10cfv 5804 . . . . 5 class (𝑛‘∅)
122cv 1474 . . . . 5 class 𝑓
1311, 12cfv 5804 . . . 4 class (𝑓‘(𝑛‘∅))
144, 8, 13cmpt 4643 . . 3 class (𝑛 ∈ (ℕ0𝑚 1𝑜) ↦ (𝑓‘(𝑛‘∅)))
152, 3, 14cmpt 4643 . 2 class (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0𝑚 1𝑜) ↦ (𝑓‘(𝑛‘∅))))
161, 15wceq 1475 1 wff toPoly1 = (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0𝑚 1𝑜) ↦ (𝑓‘(𝑛‘∅))))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator