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

Definition df-evls 16117
Description: Define the evaluation map for the polynomial algebra. The function  ( (
I evalSub  S ) `  R
) : V --> ( S  ^m  ( S  ^m  I ) ) makes sense when  I is an index set,  S is a ring,  R is a subring of  S, and where  V is the set of polynomials in  ( I mPoly  R
). This function maps an element of the formal polynomial algebra (with coefficients in  R) to a function from assignments  I --> S of the variables to elements of  S formed by evaluating the polynomial with the given assignments. (Contributed by Stefan O'Rear, 11-Mar-2015.)
Assertion
Ref Expression
df-evls  |- evalSub  =  ( i  e.  _V , 
s  e.  CRing  |->  [_ ( Base `  s )  / 
b ]_ ( r  e.  (SubRing `  s )  |-> 
[_ ( i mPoly  (
ss  r ) )  /  w ]_ ( iota_ f  e.  ( w RingHom  ( s  ^s  ( b  ^m  i
) ) ) ( ( f  o.  (algSc `  w ) )  =  ( x  e.  r 
|->  ( ( b  ^m  i )  X.  {
x } ) )  /\  ( f  o.  ( i mVar  ( ss  r ) ) )  =  ( x  e.  i 
|->  ( g  e.  ( b  ^m  i ) 
|->  ( g `  x
) ) ) ) ) ) )
Distinct variable group:    f, b, g, i, r, s, w, x

Detailed syntax breakdown of Definition df-evls
StepHypRef Expression
1 ces 16106 . 2  class evalSub
2 vi . . 3  set  i
3 vs . . 3  set  s
4 cvv 2801 . . 3  class  _V
5 ccrg 15354 . . 3  class  CRing
6 vb . . . 4  set  b
73cv 1631 . . . . 5  class  s
8 cbs 13164 . . . . 5  class  Base
97, 8cfv 5271 . . . 4  class  ( Base `  s )
10 vr . . . . 5  set  r
11 csubrg 15557 . . . . . 6  class SubRing
127, 11cfv 5271 . . . . 5  class  (SubRing `  s
)
13 vw . . . . . 6  set  w
142cv 1631 . . . . . . 7  class  i
1510cv 1631 . . . . . . . 8  class  r
16 cress 13165 . . . . . . . 8  classs
177, 15, 16co 5874 . . . . . . 7  class  ( ss  r )
18 cmpl 16105 . . . . . . 7  class mPoly
1914, 17, 18co 5874 . . . . . 6  class  ( i mPoly 
( ss  r ) )
20 vf . . . . . . . . . . 11  set  f
2120cv 1631 . . . . . . . . . 10  class  f
2213cv 1631 . . . . . . . . . . 11  class  w
23 cascl 16068 . . . . . . . . . . 11  class algSc
2422, 23cfv 5271 . . . . . . . . . 10  class  (algSc `  w )
2521, 24ccom 4709 . . . . . . . . 9  class  ( f  o.  (algSc `  w
) )
26 vx . . . . . . . . . 10  set  x
276cv 1631 . . . . . . . . . . . 12  class  b
28 cmap 6788 . . . . . . . . . . . 12  class  ^m
2927, 14, 28co 5874 . . . . . . . . . . 11  class  ( b  ^m  i )
3026cv 1631 . . . . . . . . . . . 12  class  x
3130csn 3653 . . . . . . . . . . 11  class  { x }
3229, 31cxp 4703 . . . . . . . . . 10  class  ( ( b  ^m  i )  X.  { x }
)
3326, 15, 32cmpt 4093 . . . . . . . . 9  class  ( x  e.  r  |->  ( ( b  ^m  i )  X.  { x }
) )
3425, 33wceq 1632 . . . . . . . 8  wff  ( f  o.  (algSc `  w
) )  =  ( x  e.  r  |->  ( ( b  ^m  i
)  X.  { x } ) )
35 cmvr 16104 . . . . . . . . . . 11  class mVar
3614, 17, 35co 5874 . . . . . . . . . 10  class  ( i mVar  ( ss  r ) )
3721, 36ccom 4709 . . . . . . . . 9  class  ( f  o.  ( i mVar  (
ss  r ) ) )
38 vg . . . . . . . . . . 11  set  g
3938cv 1631 . . . . . . . . . . . 12  class  g
4030, 39cfv 5271 . . . . . . . . . . 11  class  ( g `
 x )
4138, 29, 40cmpt 4093 . . . . . . . . . 10  class  ( g  e.  ( b  ^m  i )  |->  ( g `
 x ) )
4226, 14, 41cmpt 4093 . . . . . . . . 9  class  ( x  e.  i  |->  ( g  e.  ( b  ^m  i )  |->  ( g `
 x ) ) )
4337, 42wceq 1632 . . . . . . . 8  wff  ( f  o.  ( i mVar  (
ss  r ) ) )  =  ( x  e.  i  |->  ( g  e.  ( b  ^m  i
)  |->  ( g `  x ) ) )
4434, 43wa 358 . . . . . . 7  wff  ( ( f  o.  (algSc `  w ) )  =  ( x  e.  r 
|->  ( ( b  ^m  i )  X.  {
x } ) )  /\  ( f  o.  ( i mVar  ( ss  r ) ) )  =  ( x  e.  i 
|->  ( g  e.  ( b  ^m  i ) 
|->  ( g `  x
) ) ) )
45 cpws 13363 . . . . . . . . 9  class  ^s
467, 29, 45co 5874 . . . . . . . 8  class  ( s  ^s  ( b  ^m  i
) )
47 crh 15510 . . . . . . . 8  class RingHom
4822, 46, 47co 5874 . . . . . . 7  class  ( w RingHom 
( s  ^s  ( b  ^m  i ) ) )
4944, 20, 48crio 6313 . . . . . 6  class  ( iota_ f  e.  ( w RingHom  (
s  ^s  ( b  ^m  i
) ) ) ( ( f  o.  (algSc `  w ) )  =  ( x  e.  r 
|->  ( ( b  ^m  i )  X.  {
x } ) )  /\  ( f  o.  ( i mVar  ( ss  r ) ) )  =  ( x  e.  i 
|->  ( g  e.  ( b  ^m  i ) 
|->  ( g `  x
) ) ) ) )
5013, 19, 49csb 3094 . . . . 5  class  [_ (
i mPoly  ( ss  r ) )  /  w ]_ ( iota_ f  e.  ( w RingHom  ( s  ^s  (
b  ^m  i )
) ) ( ( f  o.  (algSc `  w ) )  =  ( x  e.  r 
|->  ( ( b  ^m  i )  X.  {
x } ) )  /\  ( f  o.  ( i mVar  ( ss  r ) ) )  =  ( x  e.  i 
|->  ( g  e.  ( b  ^m  i ) 
|->  ( g `  x
) ) ) ) )
5110, 12, 50cmpt 4093 . . . 4  class  ( r  e.  (SubRing `  s
)  |->  [_ ( i mPoly  (
ss  r ) )  /  w ]_ ( iota_ f  e.  ( w RingHom  ( s  ^s  ( b  ^m  i
) ) ) ( ( f  o.  (algSc `  w ) )  =  ( x  e.  r 
|->  ( ( b  ^m  i )  X.  {
x } ) )  /\  ( f  o.  ( i mVar  ( ss  r ) ) )  =  ( x  e.  i 
|->  ( g  e.  ( b  ^m  i ) 
|->  ( g `  x
) ) ) ) ) )
526, 9, 51csb 3094 . . 3  class  [_ ( Base `  s )  / 
b ]_ ( r  e.  (SubRing `  s )  |-> 
[_ ( i mPoly  (
ss  r ) )  /  w ]_ ( iota_ f  e.  ( w RingHom  ( s  ^s  ( b  ^m  i
) ) ) ( ( f  o.  (algSc `  w ) )  =  ( x  e.  r 
|->  ( ( b  ^m  i )  X.  {
x } ) )  /\  ( f  o.  ( i mVar  ( ss  r ) ) )  =  ( x  e.  i 
|->  ( g  e.  ( b  ^m  i ) 
|->  ( g `  x
) ) ) ) ) )
532, 3, 4, 5, 52cmpt2 5876 . 2  class  ( i  e.  _V ,  s  e.  CRing  |->  [_ ( Base `  s
)  /  b ]_ ( r  e.  (SubRing `  s )  |->  [_ (
i mPoly  ( ss  r ) )  /  w ]_ ( iota_ f  e.  ( w RingHom  ( s  ^s  (
b  ^m  i )
) ) ( ( f  o.  (algSc `  w ) )  =  ( x  e.  r 
|->  ( ( b  ^m  i )  X.  {
x } ) )  /\  ( f  o.  ( i mVar  ( ss  r ) ) )  =  ( x  e.  i 
|->  ( g  e.  ( b  ^m  i ) 
|->  ( g `  x
) ) ) ) ) ) )
541, 53wceq 1632 1  wff evalSub  =  ( i  e.  _V , 
s  e.  CRing  |->  [_ ( Base `  s )  / 
b ]_ ( r  e.  (SubRing `  s )  |-> 
[_ ( i mPoly  (
ss  r ) )  /  w ]_ ( iota_ f  e.  ( w RingHom  ( s  ^s  ( b  ^m  i
) ) ) ( ( f  o.  (algSc `  w ) )  =  ( x  e.  r 
|->  ( ( b  ^m  i )  X.  {
x } ) )  /\  ( f  o.  ( i mVar  ( ss  r ) ) )  =  ( x  e.  i 
|->  ( g  e.  ( b  ^m  i ) 
|->  ( g `  x
) ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  reldmevls  19417  mpfrcl  19418  evlsval  19419
  Copyright terms: Public domain W3C validator