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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ces1	|- evalSub1
1		vs	|- s
2		cvv	|- _V
3		vr	|- r
4		cbs	|- Base
5	1	cv	|- s
6	5 4	cfv	|- ( Base ` s )
7	6	cpw	|- ~P ( Base ` s )
8		vb	|- b
9		vx	|- x
10	8	cv	|- b
11		cmap	|- ^m
12		c1o	|- 1o
13	10 12 11	co	|- ( b ^m 1o )
14	10 13 11	co	|- ( b ^m ( b ^m 1o ) )
15	9	cv	|- x
16		vy	|- y
17	16	cv	|- y
18	17	csn	|- { y }
19	12 18	cxp	|- ( 1o X. { y } )
20	16 10 19	cmpt	|- ( y e. b |-> ( 1o X. { y } ) )
21	15 20	ccom	|- ( x o. ( y e. b |-> ( 1o X. { y } ) ) )
22	9 14 21	cmpt	|- ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) )
23		ces	|- evalSub
24	12 5 23	co	|- ( 1o evalSub s )
25	3	cv	|- r
26	25 24	cfv	|- ( ( 1o evalSub s ) ` r )
27	22 26	ccom	|- ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) )
28	8 6 27	csb	|- [_ ( Base ` s ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) )
29	1 3 2 7 28	cmpo	|- ( s e. _V , r e. ~P ( Base ` s ) |-> [_ ( Base ` s ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) )
30	0 29	wceq	|- evalSub1 = ( s e. _V , r e. ~P ( Base ` s ) |-> [_ ( Base ` s ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) )