Definition df-evl1 19681

Description: Define the evaluation map for the univariate polynomial algebra. The function (eval₁ ` R ) : V --> ( R ^m R ) makes sense when R is a ring, and V is the set of polynomials in (Poly<sub>1</sub> ` R ). 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.)

Assertion

Ref	Expression
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 ) ) )

Distinct variable group:   r, b, x, y

Detailed syntax breakdown of Definition df-evl1

Step	Hyp	Ref	Expression
1		ce1 19679	. 2 class eval1
2		vr	. . 3 setvar r
3		cvv 3200	. . 3 class _V
4		vb	. . . 4 setvar b
5	2	cv 1482	. . . . 5 class r
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` r )
8		vx	. . . . . 6 setvar x
9	4	cv 1482	. . . . . . 7 class b
10		c1o 7553	. . . . . . . 8 class 1o
11		cmap 7857	. . . . . . . 8 class ^m
12	9, 10, 11	co 6650	. . . . . . 7 class ( b ^m 1o )
13	9, 12, 11	co 6650	. . . . . 6 class ( b ^m ( b ^m 1o ) )
14	8	cv 1482	. . . . . . 7 class x
15		vy	. . . . . . . 8 setvar y
16	15	cv 1482	. . . . . . . . . 10 class y
17	16	csn 4177	. . . . . . . . 9 class { y }
18	10, 17	cxp 5112	. . . . . . . 8 class ( 1o X. { y } )
19	15, 9, 18	cmpt 4729	. . . . . . 7 class ( y e. b |-> ( 1o X. { y } ) )
20	14, 19	ccom 5118	. . . . . 6 class ( x o. ( y e. b |-> ( 1o X. { y } ) ) )
21	8, 13, 20	cmpt 4729	. . . . 5 class ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) )
22		cevl 19505	. . . . . 6 class eval
23	10, 5, 22	co 6650	. . . . 5 class ( 1o eval r )
24	21, 23	ccom 5118	. . . 4 class ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval r ) )
25	4, 7, 24	csb 3533	. . 3 class [_ ( Base ` r ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval r ) )
26	2, 3, 25	cmpt 4729	. 2 class ( 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 ) ) )
27	1, 26	wceq 1483	1 wff 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 ) ) )

This definition is referenced by:  evl1fval  19692