Definition df-toply1 20346

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 ↑m 1o) ↦ (𝑓‘(𝑛‘∅))))

Distinct variable group:   𝑓,𝑛

Detailed syntax breakdown of Definition df-toply1

Step	Hyp	Ref	Expression
1		ctp1 20341	. 2 class toPoly1
2		vf	. . 3 setvar 𝑓
3		cvv 3495	. . 3 class V
4		vn	. . . 4 setvar 𝑛
5		cn0 11891	. . . . 5 class ℕ0
6		c1o 8089	. . . . 5 class 1o
7		cmap 8400	. . . . 5 class ↑m
8	5, 6, 7	co 7150	. . . 4 class (ℕ0 ↑m 1o)
9		c0 4291	. . . . . 6 class ∅
10	4	cv 1532	. . . . . 6 class 𝑛
11	9, 10	cfv 6350	. . . . 5 class (𝑛‘∅)
12	2	cv 1532	. . . . 5 class 𝑓
13	11, 12	cfv 6350	. . . 4 class (𝑓‘(𝑛‘∅))
14	4, 8, 13	cmpt 5139	. . 3 class (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (𝑓‘(𝑛‘∅)))
15	2, 3, 14	cmpt 5139	. 2 class (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (𝑓‘(𝑛‘∅))))
16	1, 15	wceq 1533	1 wff toPoly1 = (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (𝑓‘(𝑛‘∅))))

This definition is referenced by: (None)