# Metamath Proof Explorer

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