This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ toPoly 1 = f ∈ V ⟼ n ∈ ℕ 0 1 𝑜 ⟼ f ⁡ n ⁡ ∅

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctp1 class toPoly 1
1 vf setvar f
2 cvv class V
3 vn setvar n
4 cn0 class ℕ 0
5 cmap class ↑ 𝑚
6 c1o class 1 𝑜
7 4 6 5 co class ℕ 0 1 𝑜
8 1 cv setvar f
9 3 cv setvar n
10 c0 class ∅
11 10 9 cfv class n ⁡ ∅
12 11 8 cfv class f ⁡ n ⁡ ∅
13 3 7 12 cmpt class n ∈ ℕ 0 1 𝑜 ⟼ f ⁡ n ⁡ ∅
14 1 2 13 cmpt class f ∈ V ⟼ n ∈ ℕ 0 1 𝑜 ⟼ f ⁡ n ⁡ ∅
15 0 14 wceq wff toPoly 1 = f ∈ V ⟼ n ∈ ℕ 0 1 𝑜 ⟼ f ⁡ n ⁡ ∅