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

Step	Hyp	Ref	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 ↑𝑚
8	5, 6, 7	co 6549	. . . 4 class (ℕ0 ↑𝑚 1𝑜)
9		c0 3874	. . . . . 6 class ∅
10	4	cv 1474	. . . . . 6 class 𝑛
11	9, 10	cfv 5804	. . . . 5 class (𝑛‘∅)
12	2	cv 1474	. . . . 5 class 𝑓
13	11, 12	cfv 5804	. . . 4 class (𝑓‘(𝑛‘∅))
14	4, 8, 13	cmpt 4643	. . 3 class (𝑛 ∈ (ℕ0 ↑𝑚 1𝑜) ↦ (𝑓‘(𝑛‘∅)))
15	2, 3, 14	cmpt 4643	. 2 class (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0 ↑𝑚 1𝑜) ↦ (𝑓‘(𝑛‘∅))))
16	1, 15	wceq 1475	1 wff toPoly1 = (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0 ↑𝑚 1𝑜) ↦ (𝑓‘(𝑛‘∅))))

This definition is referenced by: (None)