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

Definition df-evls 16101
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 16090 . 2  class evalSub
2 vi . . 3  set  i
3 vs . . 3  set  s
4 cvv 2788 . . 3  class  _V
5 ccrg 15338 . . 3  class  CRing
6 vb . . . 4  set  b
73cv 1622 . . . . 5  class  s
8 cbs 13148 . . . . 5  class  Base
97, 8cfv 5255 . . . 4  class  ( Base `  s )
10 vr . . . . 5  set  r
11 csubrg 15541 . . . . . 6  class SubRing
127, 11cfv 5255 . . . . 5  class  (SubRing `  s
)
13 vw . . . . . 6  set  w
142cv 1622 . . . . . . 7  class  i
1510cv 1622 . . . . . . . 8  class  r
16 cress 13149 . . . . . . . 8  classs
177, 15, 16co 5858 . . . . . . 7  class  ( ss  r )
18 cmpl 16089 . . . . . . 7  class mPoly
1914, 17, 18co 5858 . . . . . 6  class  ( i mPoly 
( ss  r ) )
20 vf . . . . . . . . . . 11  set  f
2120cv 1622 . . . . . . . . . 10  class  f
2213cv 1622 . . . . . . . . . . 11  class  w
23 cascl 16052 . . . . . . . . . . 11  class algSc
2422, 23cfv 5255 . . . . . . . . . 10  class  (algSc `  w )
2521, 24ccom 4693 . . . . . . . . 9  class  ( f  o.  (algSc `  w
) )
26 vx . . . . . . . . . 10  set  x
276cv 1622 . . . . . . . . . . . 12  class  b
28 cmap 6772 . . . . . . . . . . . 12  class  ^m
2927, 14, 28co 5858 . . . . . . . . . . 11  class  ( b  ^m  i )
3026cv 1622 . . . . . . . . . . . 12  class  x
3130csn 3640 . . . . . . . . . . 11  class  { x }
3229, 31cxp 4687 . . . . . . . . . 10  class  ( ( b  ^m  i )  X.  { x }
)
3326, 15, 32cmpt 4077 . . . . . . . . 9  class  ( x  e.  r  |->  ( ( b  ^m  i )  X.  { x }
) )
3425, 33wceq 1623 . . . . . . . 8  wff  ( f  o.  (algSc `  w
) )  =  ( x  e.  r  |->  ( ( b  ^m  i
)  X.  { x } ) )
35 cmvr 16088 . . . . . . . . . . 11  class mVar
3614, 17, 35co 5858 . . . . . . . . . 10  class  ( i mVar  ( ss  r ) )
3721, 36ccom 4693 . . . . . . . . 9  class  ( f  o.  ( i mVar  (
ss  r ) ) )
38 vg . . . . . . . . . . 11  set  g
3938cv 1622 . . . . . . . . . . . 12  class  g
4030, 39cfv 5255 . . . . . . . . . . 11  class  ( g `
 x )
4138, 29, 40cmpt 4077 . . . . . . . . . 10  class  ( g  e.  ( b  ^m  i )  |->  ( g `
 x ) )
4226, 14, 41cmpt 4077 . . . . . . . . 9  class  ( x  e.  i  |->  ( g  e.  ( b  ^m  i )  |->  ( g `
 x ) ) )
4337, 42wceq 1623 . . . . . . . 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 13347 . . . . . . . . 9  class  ^s
467, 29, 45co 5858 . . . . . . . 8  class  ( s  ^s  ( b  ^m  i
) )
47 crh 15494 . . . . . . . 8  class RingHom
4822, 46, 47co 5858 . . . . . . 7  class  ( w RingHom 
( s  ^s  ( b  ^m  i ) ) )
4944, 20, 48crio 6297 . . . . . 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 3081 . . . . 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 4077 . . . 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 3081 . . 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 5860 . 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 1623 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  19401  mpfrcl  19402  evlsval  19403
  Copyright terms: Public domain W3C validator