MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-evl1 Unicode version

Definition df-evl1 16277
Description: Define the evaluation map for the univariate polynomial algebra. The function  (eval1 `  R ) : V --> ( R  ^m  R ) makes sense when  R is a ring, and  V is the set of polynomials in  (Poly1 `  R ). 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.)
Assertion
Ref Expression
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 ) ) )
Distinct variable group:    r, b, x, y

Detailed syntax breakdown of Definition df-evl1
StepHypRef Expression
1 ce1 16270 . 2  class eval1
2 vr . . 3  set  r
3 cvv 2801 . . 3  class  _V
4 vb . . . 4  set  b
52cv 1631 . . . . 5  class  r
6 cbs 13164 . . . . 5  class  Base
75, 6cfv 5271 . . . 4  class  ( Base `  r )
8 vx . . . . . 6  set  x
94cv 1631 . . . . . . 7  class  b
10 c1o 6488 . . . . . . . 8  class  1o
11 cmap 6788 . . . . . . . 8  class  ^m
129, 10, 11co 5874 . . . . . . 7  class  ( b  ^m  1o )
139, 12, 11co 5874 . . . . . 6  class  ( b  ^m  ( b  ^m  1o ) )
148cv 1631 . . . . . . 7  class  x
15 vy . . . . . . . 8  set  y
1615cv 1631 . . . . . . . . . 10  class  y
1716csn 3653 . . . . . . . . 9  class  { y }
1810, 17cxp 4703 . . . . . . . 8  class  ( 1o 
X.  { y } )
1915, 9, 18cmpt 4093 . . . . . . 7  class  ( y  e.  b  |->  ( 1o 
X.  { y } ) )
2014, 19ccom 4709 . . . . . 6  class  ( x  o.  ( y  e.  b  |->  ( 1o  X.  { y } ) ) )
218, 13, 20cmpt 4093 . . . . 5  class  ( x  e.  ( b  ^m  ( b  ^m  1o ) )  |->  ( x  o.  ( y  e.  b  |->  ( 1o  X.  { y } ) ) ) )
22 cevl 16107 . . . . . 6  class eval
2310, 5, 22co 5874 . . . . 5  class  ( 1o eval 
r )
2421, 23ccom 4709 . . . 4  class  ( ( x  e.  ( b  ^m  ( b  ^m  1o ) )  |->  ( x  o.  ( y  e.  b  |->  ( 1o  X.  { y } ) ) ) )  o.  ( 1o eval  r ) )
254, 7, 24csb 3094 . . 3  class  [_ ( Base `  r )  / 
b ]_ ( ( x  e.  ( b  ^m  ( b  ^m  1o ) )  |->  ( x  o.  ( y  e.  b  |->  ( 1o  X.  { y } ) ) ) )  o.  ( 1o eval  r ) )
262, 3, 25cmpt 4093 . 2  class  ( 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 ) ) )
271, 26wceq 1632 1  wff 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 ) ) )
Colors of variables: wff set class
This definition is referenced by:  evl1fval  19426
  Copyright terms: Public domain W3C validator