Definition df-toply1 19554

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

Step	Hyp	Ref	Expression
1		ctp1 19549	. 2 class toPoly1
2		vf	. . 3 setvar 𝑓
3		cvv 3200	. . 3 class V
4		vn	. . . 4 setvar 𝑛
5		cn0 11292	. . . . 5 class ℕ0
6		c1o 7553	. . . . 5 class 1𝑜
7		cmap 7857	. . . . 5 class ↑𝑚
8	5, 6, 7	co 6650	. . . 4 class (ℕ0 ↑𝑚 1𝑜)
9		c0 3915	. . . . . 6 class ∅
10	4	cv 1482	. . . . . 6 class 𝑛
11	9, 10	cfv 5888	. . . . 5 class (𝑛‘∅)
12	2	cv 1482	. . . . 5 class 𝑓
13	11, 12	cfv 5888	. . . 4 class (𝑓‘(𝑛‘∅))
14	4, 8, 13	cmpt 4729	. . 3 class (𝑛 ∈ (ℕ0 ↑𝑚 1𝑜) ↦ (𝑓‘(𝑛‘∅)))
15	2, 3, 14	cmpt 4729	. 2 class (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0 ↑𝑚 1𝑜) ↦ (𝑓‘(𝑛‘∅))))
16	1, 15	wceq 1483	1 wff toPoly1 = (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0 ↑𝑚 1𝑜) ↦ (𝑓‘(𝑛‘∅))))

This definition is referenced by: (None)