This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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