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	$$⊢{\mathrm{evalSub}}_1=\left(s\in \mathrm{V},r\in 𝒫{\mathrm{Base}}_s⟼⦋{\mathrm{Base}}_s/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{evalSub}s\right)\left(r\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ces1	$$class{\mathrm{evalSub}}_1$$
1		vs	$$setvars$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvars$$
6	5 4	cfv	$$class{\mathrm{Base}}_s$$
7	6	cpw	$$class𝒫{\mathrm{Base}}_s$$
8		vb	$$setvarb$$
9		vx	$$setvarx$$
10	8	cv	$$setvarb$$
11		cmap	$$class{\uparrow }_{𝑚}$$
12		c1o	$$class{1}_{𝑜}$$
13	10 12 11	co	$$class\left(b^{1_{𝑜}}\right)$$
14	10 13 11	co	$$class\left(b^{\left(b^{1_{𝑜}}\right)}\right)$$
15	9	cv	$$setvarx$$
16		vy	$$setvary$$
17	16	cv	$$setvary$$
18	17	csn	$$class\left\{y\right\}$$
19	12 18	cxp	$$class\left(1_{𝑜}\times \left\{y\right\}\right)$$
20	16 10 19	cmpt	$$class\left(y\in b⟼1_{𝑜}\times \left\{y\right\}\right)$$
21	15 20	ccom	$$class\left(x\circ \left(y\in b⟼1_{𝑜}\times \left\{y\right\}\right)\right)$$
22	9 14 21	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)$$
23		ces	$$class\mathrm{evalSub}$$
24	12 5 23	co	$$class\left(1_{𝑜}\mathrm{evalSub}s\right)$$
25	3	cv	$$setvarr$$
26	25 24	cfv	$$class\left(1_{𝑜}\mathrm{evalSub}s\right)\left(r\right)$$
27	22 26	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{evalSub}s\right)\left(r\right)\right)$$
28	8 6 27	csb	$$class⦋{\mathrm{Base}}_s/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{evalSub}s\right)\left(r\right)\right)$$
29	1 3 2 7 28	cmpo	$$class\left(s\in \mathrm{V},r\in 𝒫{\mathrm{Base}}_s⟼⦋{\mathrm{Base}}_s/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{evalSub}s\right)\left(r\right)\right)\right)$$
30	0 29	wceq	$$wff{\mathrm{evalSub}}_1=\left(s\in \mathrm{V},r\in 𝒫{\mathrm{Base}}_s⟼⦋{\mathrm{Base}}_s/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{evalSub}s\right)\left(r\right)\right)\right)$$