Definition df-toply1

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)

	Ref	Expression
Assertion	df-toply1	⊢ toPoly1 = ( 𝑓 ∈ V ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑓 ‘ ( 𝑛 ‘ ∅ ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctp1	⊢ toPoly1
1		vf	⊢ 𝑓
2		cvv	⊢ V
3		vn	⊢ 𝑛
4		cn0	⊢ ℕ0
5		cmap	⊢ ↑m
6		c1o	⊢ 1o
7	4 6 5	co	⊢ ( ℕ0 ↑m 1o )
8	1	cv	⊢ 𝑓
9	3	cv	⊢ 𝑛
10		c0	⊢ ∅
11	10 9	cfv	⊢ ( 𝑛 ‘ ∅ )
12	11 8	cfv	⊢ ( 𝑓 ‘ ( 𝑛 ‘ ∅ ) )
13	3 7 12	cmpt	⊢ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑓 ‘ ( 𝑛 ‘ ∅ ) ) )
14	1 2 13	cmpt	⊢ ( 𝑓 ∈ V ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑓 ‘ ( 𝑛 ‘ ∅ ) ) ) )
15	0 14	wceq	⊢ toPoly1 = ( 𝑓 ∈ V ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑓 ‘ ( 𝑛 ‘ ∅ ) ) ) )