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

Definition df-evls1 19501
 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 = (𝑠 ∈ V, 𝑟 ∈ 𝒫 (Base‘𝑠) ↦ (Base‘𝑠) / 𝑏((𝑥 ∈ (𝑏𝑚 (𝑏𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1𝑜 × {𝑦})))) ∘ ((1𝑜 evalSub 𝑠)‘𝑟)))
Distinct variable group:   𝑟,𝑏,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-evls1
StepHypRef Expression
1 ces1 19499 . 2 class evalSub1
2 vs . . 3 setvar 𝑠
3 vr . . 3 setvar 𝑟
4 cvv 3173 . . 3 class V
52cv 1474 . . . . 5 class 𝑠
6 cbs 15695 . . . . 5 class Base
75, 6cfv 5804 . . . 4 class (Base‘𝑠)
87cpw 4108 . . 3 class 𝒫 (Base‘𝑠)
9 vb . . . 4 setvar 𝑏
10 vx . . . . . 6 setvar 𝑥
119cv 1474 . . . . . . 7 class 𝑏
12 c1o 7440 . . . . . . . 8 class 1𝑜
13 cmap 7744 . . . . . . . 8 class 𝑚
1411, 12, 13co 6549 . . . . . . 7 class (𝑏𝑚 1𝑜)
1511, 14, 13co 6549 . . . . . 6 class (𝑏𝑚 (𝑏𝑚 1𝑜))
1610cv 1474 . . . . . . 7 class 𝑥
17 vy . . . . . . . 8 setvar 𝑦
1817cv 1474 . . . . . . . . . 10 class 𝑦
1918csn 4125 . . . . . . . . 9 class {𝑦}
2012, 19cxp 5036 . . . . . . . 8 class (1𝑜 × {𝑦})
2117, 11, 20cmpt 4643 . . . . . . 7 class (𝑦𝑏 ↦ (1𝑜 × {𝑦}))
2216, 21ccom 5042 . . . . . 6 class (𝑥 ∘ (𝑦𝑏 ↦ (1𝑜 × {𝑦})))
2310, 15, 22cmpt 4643 . . . . 5 class (𝑥 ∈ (𝑏𝑚 (𝑏𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1𝑜 × {𝑦}))))
243cv 1474 . . . . . 6 class 𝑟
25 ces 19325 . . . . . . 7 class evalSub
2612, 5, 25co 6549 . . . . . 6 class (1𝑜 evalSub 𝑠)
2724, 26cfv 5804 . . . . 5 class ((1𝑜 evalSub 𝑠)‘𝑟)
2823, 27ccom 5042 . . . 4 class ((𝑥 ∈ (𝑏𝑚 (𝑏𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1𝑜 × {𝑦})))) ∘ ((1𝑜 evalSub 𝑠)‘𝑟))
299, 7, 28csb 3499 . . 3 class (Base‘𝑠) / 𝑏((𝑥 ∈ (𝑏𝑚 (𝑏𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1𝑜 × {𝑦})))) ∘ ((1𝑜 evalSub 𝑠)‘𝑟))
302, 3, 4, 8, 29cmpt2 6551 . 2 class (𝑠 ∈ V, 𝑟 ∈ 𝒫 (Base‘𝑠) ↦ (Base‘𝑠) / 𝑏((𝑥 ∈ (𝑏𝑚 (𝑏𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1𝑜 × {𝑦})))) ∘ ((1𝑜 evalSub 𝑠)‘𝑟)))
311, 30wceq 1475 1 wff evalSub1 = (𝑠 ∈ V, 𝑟 ∈ 𝒫 (Base‘𝑠) ↦ (Base‘𝑠) / 𝑏((𝑥 ∈ (𝑏𝑚 (𝑏𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦𝑏 ↦ (1𝑜 × {𝑦})))) ∘ ((1𝑜 evalSub 𝑠)‘𝑟)))
 Colors of variables: wff setvar class This definition is referenced by:  reldmevls1  19503  ply1frcl  19504  evls1fval  19505
 Copyright terms: Public domain W3C validator