Definition df-evls1 19680

Description: Define the evaluation map for the univariate polynomial algebra. The function ( S evalSub₁ 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 (Poly₁ ` R ). 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.)

Assertion

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

Distinct variable group:   r, b, s, x, y

Detailed syntax breakdown of Definition df-evls1

Step	Hyp	Ref	Expression
1		ces1 19678	. 2 class evalSub1
2		vs	. . 3 setvar s
3		vr	. . 3 setvar r
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . . 5 class s
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` s )
8	7	cpw 4158	. . 3 class ~P ( Base ` s )
9		vb	. . . 4 setvar b
10		vx	. . . . . 6 setvar x
11	9	cv 1482	. . . . . . 7 class b
12		c1o 7553	. . . . . . . 8 class 1o
13		cmap 7857	. . . . . . . 8 class ^m
14	11, 12, 13	co 6650	. . . . . . 7 class ( b ^m 1o )
15	11, 14, 13	co 6650	. . . . . 6 class ( b ^m ( b ^m 1o ) )
16	10	cv 1482	. . . . . . 7 class x
17		vy	. . . . . . . 8 setvar y
18	17	cv 1482	. . . . . . . . . 10 class y
19	18	csn 4177	. . . . . . . . 9 class { y }
20	12, 19	cxp 5112	. . . . . . . 8 class ( 1o X. { y } )
21	17, 11, 20	cmpt 4729	. . . . . . 7 class ( y e. b |-> ( 1o X. { y } ) )
22	16, 21	ccom 5118	. . . . . 6 class ( x o. ( y e. b |-> ( 1o X. { y } ) ) )
23	10, 15, 22	cmpt 4729	. . . . 5 class ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) )
24	3	cv 1482	. . . . . 6 class r
25		ces 19504	. . . . . . 7 class evalSub
26	12, 5, 25	co 6650	. . . . . 6 class ( 1o evalSub s )
27	24, 26	cfv 5888	. . . . 5 class ( ( 1o evalSub s ) ` r )
28	23, 27	ccom 5118	. . . 4 class ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) )
29	9, 7, 28	csb 3533	. . 3 class [_ ( Base ` s ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) )
30	2, 3, 4, 8, 29	cmpt2 6652	. 2 class ( 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 ) ) )
31	1, 30	wceq 1483	1 wff 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 ) ) )

This definition is referenced by:  reldmevls1  19682  ply1frcl  19683  evls1fval  19684