This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC LINEAR ALGEBRA Abstract multivariate polynomials Univariate polynomials 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 ) ↦ ( 𝑓 ‘ ( 𝑛 ‘ ∅ ) ) ) )