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 evalSub1=sV,r𝒫BasesBases/bxbb1𝑜xyb1𝑜×y1𝑜evalSubsr

Detailed syntax breakdown

Step Hyp Ref Expression
0 ces1 classevalSub1
1 vs setvars
2 cvv classV
3 vr setvarr
4 cbs classBase
5 1 cv setvars
6 5 4 cfv classBases
7 6 cpw class𝒫Bases
8 vb setvarb
9 vx setvarx
10 8 cv setvarb
11 cmap class𝑚
12 c1o class1𝑜
13 10 12 11 co classb1𝑜
14 10 13 11 co classbb1𝑜
15 9 cv setvarx
16 vy setvary
17 16 cv setvary
18 17 csn classy
19 12 18 cxp class1𝑜×y
20 16 10 19 cmpt classyb1𝑜×y
21 15 20 ccom classxyb1𝑜×y
22 9 14 21 cmpt classxbb1𝑜xyb1𝑜×y
23 ces classevalSub
24 12 5 23 co class1𝑜evalSubs
25 3 cv setvarr
26 25 24 cfv class1𝑜evalSubsr
27 22 26 ccom classxbb1𝑜xyb1𝑜×y1𝑜evalSubsr
28 8 6 27 csb classBases/bxbb1𝑜xyb1𝑜×y1𝑜evalSubsr
29 1 3 2 7 28 cmpo classsV,r𝒫BasesBases/bxbb1𝑜xyb1𝑜×y1𝑜evalSubsr
30 0 29 wceq wffevalSub1=sV,r𝒫BasesBases/bxbb1𝑜xyb1𝑜×y1𝑜evalSubsr