# Metamath Proof Explorer

## 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 ) ) )`