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

Definition df-evls1 16276
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  (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  S into an element of  S formed by evaluating the polynomial with the given assignment. (Contributed by Mario Carneiro, 12-Jun-2015.)
Assertion
Ref Expression
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 ) ) )
Distinct variable group:    r, b, s, x, y

Detailed syntax breakdown of Definition df-evls1
StepHypRef Expression
1 ces1 16269 . 2  class evalSub1
2 vs . . 3  set  s
3 vr . . 3  set  r
4 cvv 2801 . . 3  class  _V
52cv 1631 . . . . 5  class  s
6 cbs 13164 . . . . 5  class  Base
75, 6cfv 5271 . . . 4  class  ( Base `  s )
87cpw 3638 . . 3  class  ~P ( Base `  s )
9 vb . . . 4  set  b
10 vx . . . . . 6  set  x
119cv 1631 . . . . . . 7  class  b
12 c1o 6488 . . . . . . . 8  class  1o
13 cmap 6788 . . . . . . . 8  class  ^m
1411, 12, 13co 5874 . . . . . . 7  class  ( b  ^m  1o )
1511, 14, 13co 5874 . . . . . 6  class  ( b  ^m  ( b  ^m  1o ) )
1610cv 1631 . . . . . . 7  class  x
17 vy . . . . . . . 8  set  y
1817cv 1631 . . . . . . . . . 10  class  y
1918csn 3653 . . . . . . . . 9  class  { y }
2012, 19cxp 4703 . . . . . . . 8  class  ( 1o 
X.  { y } )
2117, 11, 20cmpt 4093 . . . . . . 7  class  ( y  e.  b  |->  ( 1o 
X.  { y } ) )
2216, 21ccom 4709 . . . . . 6  class  ( x  o.  ( y  e.  b  |->  ( 1o  X.  { y } ) ) )
2310, 15, 22cmpt 4093 . . . . 5  class  ( x  e.  ( b  ^m  ( b  ^m  1o ) )  |->  ( x  o.  ( y  e.  b  |->  ( 1o  X.  { y } ) ) ) )
243cv 1631 . . . . . 6  class  r
25 ces 16106 . . . . . . 7  class evalSub
2612, 5, 25co 5874 . . . . . 6  class  ( 1o evalSub  s )
2724, 26cfv 5271 . . . . 5  class  ( ( 1o evalSub  s ) `  r )
2823, 27ccom 4709 . . . 4  class  ( ( x  e.  ( b  ^m  ( b  ^m  1o ) )  |->  ( x  o.  ( y  e.  b  |->  ( 1o  X.  { y } ) ) ) )  o.  ( ( 1o evalSub  s ) `
 r ) )
299, 7, 28csb 3094 . . 3  class  [_ ( Base `  s )  / 
b ]_ ( ( x  e.  ( b  ^m  ( b  ^m  1o ) )  |->  ( x  o.  ( y  e.  b  |->  ( 1o  X.  { y } ) ) ) )  o.  ( ( 1o evalSub  s ) `
 r ) )
302, 3, 4, 8, 29cmpt2 5876 . 2  class  ( 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 ) ) )
311, 30wceq 1632 1  wff 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 ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator