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

Definition df-evls 17610
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 17608 . 2  class evalSub
2 vi . . 3  setvar  i
3 vs . . 3  setvar  s
4 cvv 2993 . . 3  class  _V
5 ccrg 16668 . . 3  class  CRing
6 vb . . . 4  setvar  b
73cv 1368 . . . . 5  class  s
8 cbs 14195 . . . . 5  class  Base
97, 8cfv 5439 . . . 4  class  ( Base `  s )
10 vr . . . . 5  setvar  r
11 csubrg 16883 . . . . . 6  class SubRing
127, 11cfv 5439 . . . . 5  class  (SubRing `  s
)
13 vw . . . . . 6  setvar  w
142cv 1368 . . . . . . 7  class  i
1510cv 1368 . . . . . . . 8  class  r
16 cress 14196 . . . . . . . 8  classs
177, 15, 16co 6112 . . . . . . 7  class  ( ss  r )
18 cmpl 17442 . . . . . . 7  class mPoly
1914, 17, 18co 6112 . . . . . 6  class  ( i mPoly 
( ss  r ) )
20 vf . . . . . . . . . . 11  setvar  f
2120cv 1368 . . . . . . . . . 10  class  f
2213cv 1368 . . . . . . . . . . 11  class  w
23 cascl 17405 . . . . . . . . . . 11  class algSc
2422, 23cfv 5439 . . . . . . . . . 10  class  (algSc `  w )
2521, 24ccom 4865 . . . . . . . . 9  class  ( f  o.  (algSc `  w
) )
26 vx . . . . . . . . . 10  setvar  x
276cv 1368 . . . . . . . . . . . 12  class  b
28 cmap 7235 . . . . . . . . . . . 12  class  ^m
2927, 14, 28co 6112 . . . . . . . . . . 11  class  ( b  ^m  i )
3026cv 1368 . . . . . . . . . . . 12  class  x
3130csn 3898 . . . . . . . . . . 11  class  { x }
3229, 31cxp 4859 . . . . . . . . . 10  class  ( ( b  ^m  i )  X.  { x }
)
3326, 15, 32cmpt 4371 . . . . . . . . 9  class  ( x  e.  r  |->  ( ( b  ^m  i )  X.  { x }
) )
3425, 33wceq 1369 . . . . . . . 8  wff  ( f  o.  (algSc `  w
) )  =  ( x  e.  r  |->  ( ( b  ^m  i
)  X.  { x } ) )
35 cmvr 17441 . . . . . . . . . . 11  class mVar
3614, 17, 35co 6112 . . . . . . . . . 10  class  ( i mVar  ( ss  r ) )
3721, 36ccom 4865 . . . . . . . . 9  class  ( f  o.  ( i mVar  (
ss  r ) ) )
38 vg . . . . . . . . . . 11  setvar  g
3938cv 1368 . . . . . . . . . . . 12  class  g
4030, 39cfv 5439 . . . . . . . . . . 11  class  ( g `
 x )
4138, 29, 40cmpt 4371 . . . . . . . . . 10  class  ( g  e.  ( b  ^m  i )  |->  ( g `
 x ) )
4226, 14, 41cmpt 4371 . . . . . . . . 9  class  ( x  e.  i  |->  ( g  e.  ( b  ^m  i )  |->  ( g `
 x ) ) )
4337, 42wceq 1369 . . . . . . . 8  wff  ( f  o.  ( i mVar  (
ss  r ) ) )  =  ( x  e.  i  |->  ( g  e.  ( b  ^m  i
)  |->  ( g `  x ) ) )
4434, 43wa 369 . . . . . . 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 14406 . . . . . . . . 9  class  ^s
467, 29, 45co 6112 . . . . . . . 8  class  ( s  ^s  ( b  ^m  i
) )
47 crh 16826 . . . . . . . 8  class RingHom
4822, 46, 47co 6112 . . . . . . 7  class  ( w RingHom 
( s  ^s  ( b  ^m  i ) ) )
4944, 20, 48crio 6072 . . . . . 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 3309 . . . . 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 4371 . . . 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 3309 . . 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 6114 . 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 1369 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 setvar class
This definition is referenced by:  reldmevls  17625  mpfrcl  17626  evlsval  17627
  Copyright terms: Public domain W3C validator