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

Definition df-evls1 18226
 Description: Define the evaluation map for the univariate polynomial algebra. The function evalSub1 makes sense when is a ring and is a subring of , and where is the set of polynomials in Poly1. This function maps an element of the formal polynomial algebra (with coefficients in ) to a function from assignments to the variable from into an element of formed by evaluating the polynomial with the given assignment. (Contributed by Mario Carneiro, 12-Jun-2015.)
Assertion
Ref Expression
df-evls1 evalSub1 evalSub
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-evls1
StepHypRef Expression
1 ces1 18224 . 2 evalSub1
2 vs . . 3
3 vr . . 3
4 cvv 3095 . . 3
52cv 1382 . . . . 5
6 cbs 14509 . . . . 5
75, 6cfv 5578 . . . 4
87cpw 3997 . . 3
9 vb . . . 4
10 vx . . . . . 6
119cv 1382 . . . . . . 7
12 c1o 7125 . . . . . . . 8
13 cmap 7422 . . . . . . . 8
1411, 12, 13co 6281 . . . . . . 7
1511, 14, 13co 6281 . . . . . 6
1610cv 1382 . . . . . . 7
17 vy . . . . . . . 8
1817cv 1382 . . . . . . . . . 10
1918csn 4014 . . . . . . . . 9
2012, 19cxp 4987 . . . . . . . 8
2117, 11, 20cmpt 4495 . . . . . . 7
2216, 21ccom 4993 . . . . . 6
2310, 15, 22cmpt 4495 . . . . 5
243cv 1382 . . . . . 6
25 ces 18043 . . . . . . 7 evalSub
2612, 5, 25co 6281 . . . . . 6 evalSub
2724, 26cfv 5578 . . . . 5 evalSub
2823, 27ccom 4993 . . . 4 evalSub
299, 7, 28csb 3420 . . 3 evalSub
302, 3, 4, 8, 29cmpt2 6283 . 2 evalSub
311, 30wceq 1383 1 evalSub1 evalSub
 Colors of variables: wff setvar class This definition is referenced by:  reldmevls1  18228  ply1frcl  18229  evls1fval  18230
 Copyright terms: Public domain W3C validator