# Metamath Proof Explorer

## Definition df-evl1

Description: Define the evaluation map for the univariate polynomial algebra. The function ( eval1R ) : V --> ( R ^m R ) makes sense when R is a ring, and V is the set of polynomials in ( Poly1R ) . This function maps an element of the formal polynomial algebra (with coefficients in R ) to a function from assignments to the variable from R into an element of R formed by evaluating the polynomial with the given assignment. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Assertion df-evl1

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ce1 ${class}{\mathrm{eval}}_{1}$
1 vr ${setvar}{r}$
2 cvv ${class}\mathrm{V}$
3 cbs ${class}\mathrm{Base}$
4 1 cv ${setvar}{r}$
5 4 3 cfv ${class}{\mathrm{Base}}_{{r}}$
6 vb ${setvar}{b}$
7 vx ${setvar}{x}$
8 6 cv ${setvar}{b}$
9 cmap ${class}{↑}_{𝑚}$
10 c1o ${class}{1}_{𝑜}$
11 8 10 9 co ${class}\left({{b}}^{{1}_{𝑜}}\right)$
12 8 11 9 co ${class}\left({{b}}^{\left({{b}}^{{1}_{𝑜}}\right)}\right)$
13 7 cv ${setvar}{x}$
14 vy ${setvar}{y}$
15 14 cv ${setvar}{y}$
16 15 csn ${class}\left\{{y}\right\}$
17 10 16 cxp ${class}\left({1}_{𝑜}×\left\{{y}\right\}\right)$
18 14 8 17 cmpt ${class}\left({y}\in {b}⟼{1}_{𝑜}×\left\{{y}\right\}\right)$
19 13 18 ccom ${class}\left({x}\circ \left({y}\in {b}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)$
20 7 12 19 cmpt ${class}\left({x}\in \left({{b}}^{\left({{b}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {b}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)$
21 cevl ${class}\mathrm{eval}$
22 10 4 21 co ${class}\left({1}_{𝑜}\mathrm{eval}{r}\right)$
23 20 22 ccom ${class}\left(\left({x}\in \left({{b}}^{\left({{b}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {b}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ \left({1}_{𝑜}\mathrm{eval}{r}\right)\right)$
24 6 5 23 csb
25 1 2 24 cmpt
26 0 25 wceq