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	|- eval1 = ( r e. _V |-> [_ ( Base ` r ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval r ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ce1	|- eval1
1		vr	|- r
2		cvv	|- _V
3		cbs	|- Base
4	1	cv	|- r
5	4 3	cfv	|- ( Base ` r )
6		vb	|- b
7		vx	|- x
8	6	cv	|- b
9		cmap	|- ^m
10		c1o	|- 1o
11	8 10 9	co	|- ( b ^m 1o )
12	8 11 9	co	|- ( b ^m ( b ^m 1o ) )
13	7	cv	|- x
14		vy	|- y
15	14	cv	|- y
16	15	csn	|- { y }
17	10 16	cxp	|- ( 1o X. { y } )
18	14 8 17	cmpt	|- ( y e. b |-> ( 1o X. { y } ) )
19	13 18	ccom	|- ( x o. ( y e. b |-> ( 1o X. { y } ) ) )
20	7 12 19	cmpt	|- ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) )
21		cevl	|- eval
22	10 4 21	co	|- ( 1o eval r )
23	20 22	ccom	|- ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval r ) )
24	6 5 23	csb	|- [_ ( Base ` r ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval r ) )
25	1 2 24	cmpt	|- ( r e. _V |-> [_ ( Base ` r ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval r ) ) )
26	0 25	wceq	|- eval1 = ( r e. _V |-> [_ ( Base ` r ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval r ) ) )