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

Definition df-evls 17970
 Description: Define the evaluation map for the polynomial algebra. The function evalSub makes sense when is an index set, is a ring, is a subring of , and where is the set of polynomials in mPoly . This function maps an element of the formal polynomial algebra (with coefficients in ) to a function from assignments of the variables to elements of formed by evaluating the polynomial with the given assignments. (Contributed by Stefan O'Rear, 11-Mar-2015.)
Assertion
Ref Expression
df-evls evalSub SubRing mPoly s RingHom s algSc mVar s
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-evls
StepHypRef Expression
1 ces 17968 . 2 evalSub
2 vi . . 3
3 vs . . 3
4 cvv 3113 . . 3
5 ccrg 17001 . . 3
6 vb . . . 4
73cv 1378 . . . . 5
8 cbs 14490 . . . . 5
97, 8cfv 5588 . . . 4
10 vr . . . . 5
11 csubrg 17225 . . . . . 6 SubRing
127, 11cfv 5588 . . . . 5 SubRing
13 vw . . . . . 6
142cv 1378 . . . . . . 7
1510cv 1378 . . . . . . . 8
16 cress 14491 . . . . . . . 8 s
177, 15, 16co 6284 . . . . . . 7 s
18 cmpl 17801 . . . . . . 7 mPoly
1914, 17, 18co 6284 . . . . . 6 mPoly s
20 vf . . . . . . . . . . 11
2120cv 1378 . . . . . . . . . 10
2213cv 1378 . . . . . . . . . . 11
23 cascl 17759 . . . . . . . . . . 11 algSc
2422, 23cfv 5588 . . . . . . . . . 10 algSc
2521, 24ccom 5003 . . . . . . . . 9 algSc
26 vx . . . . . . . . . 10
276cv 1378 . . . . . . . . . . . 12
28 cmap 7420 . . . . . . . . . . . 12
2927, 14, 28co 6284 . . . . . . . . . . 11
3026cv 1378 . . . . . . . . . . . 12
3130csn 4027 . . . . . . . . . . 11
3229, 31cxp 4997 . . . . . . . . . 10
3326, 15, 32cmpt 4505 . . . . . . . . 9
3425, 33wceq 1379 . . . . . . . 8 algSc
35 cmvr 17800 . . . . . . . . . . 11 mVar
3614, 17, 35co 6284 . . . . . . . . . 10 mVar s
3721, 36ccom 5003 . . . . . . . . 9 mVar s
38 vg . . . . . . . . . . 11
3938cv 1378 . . . . . . . . . . . 12
4030, 39cfv 5588 . . . . . . . . . . 11
4138, 29, 40cmpt 4505 . . . . . . . . . 10
4226, 14, 41cmpt 4505 . . . . . . . . 9
4337, 42wceq 1379 . . . . . . . 8 mVar s
4434, 43wa 369 . . . . . . 7 algSc mVar s
45 cpws 14702 . . . . . . . . 9 s
467, 29, 45co 6284 . . . . . . . 8 s
47 crh 17162 . . . . . . . 8 RingHom
4822, 46, 47co 6284 . . . . . . 7 RingHom s
4944, 20, 48crio 6244 . . . . . 6 RingHom s algSc mVar s
5013, 19, 49csb 3435 . . . . 5 mPoly s RingHom s algSc mVar s
5110, 12, 50cmpt 4505 . . . 4 SubRing mPoly s RingHom s algSc mVar s
526, 9, 51csb 3435 . . 3 SubRing mPoly s RingHom s algSc mVar s
532, 3, 4, 5, 52cmpt2 6286 . 2 SubRing mPoly s RingHom s algSc mVar s
541, 53wceq 1379 1 evalSub SubRing mPoly s RingHom s algSc mVar s
 Colors of variables: wff setvar class This definition is referenced by:  reldmevls  17985  mpfrcl  17986  evlsval  17987
 Copyright terms: Public domain W3C validator