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

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