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	$$⊢{\mathrm{eval}}_1=\left(r\in \mathrm{V}⟼⦋{\mathrm{Base}}_r/b⦌\left(\left(x\in \left(b^{\left(b^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in b⟼1_{𝑜}\times \left\{y\right\}\right)\right)\circ \left(1_{𝑜}\mathrm{eval}r\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ce1	$$class{\mathrm{eval}}_1$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvarr$$
5	4 3	cfv	$$class{\mathrm{Base}}_r$$
6		vb	$$setvarb$$
7		vx	$$setvarx$$
8	6	cv	$$setvarb$$
9		cmap	$$class{\uparrow }_{𝑚}$$
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	$$setvarx$$
14		vy	$$setvary$$
15	14	cv	$$setvary$$
16	15	csn	$$class\left\{y\right\}$$
17	10 16	cxp	$$class\left(1_{𝑜}\times \left\{y\right\}\right)$$
18	14 8 17	cmpt	$$class\left(y\in b⟼1_{𝑜}\times \left\{y\right\}\right)$$
19	13 18	ccom	$$class\left(x\circ \left(y\in b⟼1_{𝑜}\times \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_{𝑜}\times \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_{𝑜}\times \left\{y\right\}\right)\right)\circ \left(1_{𝑜}\mathrm{eval}r\right)\right)$$
24	6 5 23	csb	$$class⦋{\mathrm{Base}}_r/b⦌\left(\left(x\in \left(b^{\left(b^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in b⟼1_{𝑜}\times \left\{y\right\}\right)\right)\circ \left(1_{𝑜}\mathrm{eval}r\right)\right)$$
25	1 2 24	cmpt	$$class\left(r\in \mathrm{V}⟼⦋{\mathrm{Base}}_r/b⦌\left(\left(x\in \left(b^{\left(b^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in b⟼1_{𝑜}\times \left\{y\right\}\right)\right)\circ \left(1_{𝑜}\mathrm{eval}r\right)\right)\right)$$
26	0 25	wceq	$$wff{\mathrm{eval}}_1=\left(r\in \mathrm{V}⟼⦋{\mathrm{Base}}_r/b⦌\left(\left(x\in \left(b^{\left(b^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in b⟼1_{𝑜}\times \left\{y\right\}\right)\right)\circ \left(1_{𝑜}\mathrm{eval}r\right)\right)\right)$$