# Metamath Proof Explorer

## Definition df-evls1

Description: Define the evaluation map for the univariate polynomial algebra. The function ( S evalSub1 R ) : V --> ( S ^m S ) makes sense when S is a ring and R is a subring of S , and where 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 S into an element of S formed by evaluating the polynomial with the given assignment. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Assertion df-evls1

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ces1 $class evalSub 1$
1 vs $setvar s$
2 cvv $class V$
3 vr $setvar r$
4 cbs $class Base$
5 1 cv $setvar s$
6 5 4 cfv $class Base s$
7 6 cpw $class 𝒫 Base s$
8 vb $setvar b$
9 vx $setvar x$
10 8 cv $setvar b$
11 cmap $class ↑ 𝑚$
12 c1o $class 1 𝑜$
13 10 12 11 co $class b 1 𝑜$
14 10 13 11 co $class b b 1 𝑜$
15 9 cv $setvar x$
16 vy $setvar y$
17 16 cv $setvar y$
18 17 csn $class y$
19 12 18 cxp $class 1 𝑜 × y$
20 16 10 19 cmpt $class y ∈ b ⟼ 1 𝑜 × y$
21 15 20 ccom $class x ∘ y ∈ b ⟼ 1 𝑜 × y$
22 9 14 21 cmpt $class x ∈ b b 1 𝑜 ⟼ x ∘ y ∈ b ⟼ 1 𝑜 × y$
23 ces $class evalSub$
24 12 5 23 co $class 1 𝑜 evalSub s$
25 3 cv $setvar r$
26 25 24 cfv $class 1 𝑜 evalSub s ⁡ r$
27 22 26 ccom $class x ∈ b b 1 𝑜 ⟼ x ∘ y ∈ b ⟼ 1 𝑜 × y ∘ 1 𝑜 evalSub s ⁡ r$
28 8 6 27 csb
29 1 3 2 7 28 cmpo
30 0 29 wceq