Definition df-evls1 19501

Description: Define the evaluation map for the univariate polynomial algebra. The function (𝑆 evalSub₁ 𝑅):𝑉⟶(𝑆 ↑_𝑚 𝑆) makes sense when 𝑆 is a ring and 𝑅 is a subring of 𝑆, and where 𝑉 is the set of polynomials in (Poly₁‘𝑅). 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

Step	Hyp	Ref	Expression
1		ces1 19499	. 2 class evalSub1
2		vs	. . 3 setvar 𝑠
3		vr	. . 3 setvar 𝑟
4		cvv 3173	. . 3 class V
5	2	cv 1474	. . . . 5 class 𝑠
6		cbs 15695	. . . . 5 class Base
7	5, 6	cfv 5804	. . . 4 class (Base‘𝑠)
8	7	cpw 4108	. . 3 class 𝒫 (Base‘𝑠)
9		vb	. . . 4 setvar 𝑏
10		vx	. . . . . 6 setvar 𝑥
11	9	cv 1474	. . . . . . 7 class 𝑏
12		c1o 7440	. . . . . . . 8 class 1𝑜
13		cmap 7744	. . . . . . . 8 class ↑𝑚
14	11, 12, 13	co 6549	. . . . . . 7 class (𝑏 ↑𝑚 1𝑜)
15	11, 14, 13	co 6549	. . . . . 6 class (𝑏 ↑𝑚 (𝑏 ↑𝑚 1𝑜))
16	10	cv 1474	. . . . . . 7 class 𝑥
17		vy	. . . . . . . 8 setvar 𝑦
18	17	cv 1474	. . . . . . . . . 10 class 𝑦
19	18	csn 4125	. . . . . . . . 9 class {𝑦}
20	12, 19	cxp 5036	. . . . . . . 8 class (1𝑜 × {𝑦})
21	17, 11, 20	cmpt 4643	. . . . . . 7 class (𝑦 ∈ 𝑏 ↦ (1𝑜 × {𝑦}))
22	16, 21	ccom 5042	. . . . . 6 class (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 × {𝑦})))
23	10, 15, 22	cmpt 4643	. . . . 5 class (𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 × {𝑦}))))
24	3	cv 1474	. . . . . 6 class 𝑟
25		ces 19325	. . . . . . 7 class evalSub
26	12, 5, 25	co 6549	. . . . . 6 class (1𝑜 evalSub 𝑠)
27	24, 26	cfv 5804	. . . . 5 class ((1𝑜 evalSub 𝑠)‘𝑟)
28	23, 27	ccom 5042	. . . 4 class ((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 × {𝑦})))) ∘ ((1𝑜 evalSub 𝑠)‘𝑟))
29	9, 7, 28	csb 3499	. . 3 class ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 × {𝑦})))) ∘ ((1𝑜 evalSub 𝑠)‘𝑟))
30	2, 3, 4, 8, 29	cmpt2 6551	. 2 class (𝑠 ∈ V, 𝑟 ∈ 𝒫 (Base‘𝑠) ↦ ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 × {𝑦})))) ∘ ((1𝑜 evalSub 𝑠)‘𝑟)))
31	1, 30	wceq 1475	1 wff evalSub1 = (𝑠 ∈ V, 𝑟 ∈ 𝒫 (Base‘𝑠) ↦ ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 × {𝑦})))) ∘ ((1𝑜 evalSub 𝑠)‘𝑟)))

This definition is referenced by:  reldmevls1  19503  ply1frcl  19504  evls1fval  19505