Definition df-evls1 20470

Description: Define the evaluation map for the univariate polynomial algebra. The function (𝑆 evalSub₁ 𝑅):𝑉⟶(𝑆 ↑_m 𝑆) 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‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))

Distinct variable group:   𝑟,𝑏,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-evls1

Step	Hyp	Ref	Expression
1		ces1 20468	. 2 class evalSub1
2		vs	. . 3 setvar 𝑠
3		vr	. . 3 setvar 𝑟
4		cvv 3493	. . 3 class V
5	2	cv 1530	. . . . 5 class 𝑠
6		cbs 16475	. . . . 5 class Base
7	5, 6	cfv 6348	. . . 4 class (Base‘𝑠)
8	7	cpw 4537	. . 3 class 𝒫 (Base‘𝑠)
9		vb	. . . 4 setvar 𝑏
10		vx	. . . . . 6 setvar 𝑥
11	9	cv 1530	. . . . . . 7 class 𝑏
12		c1o 8087	. . . . . . . 8 class 1o
13		cmap 8398	. . . . . . . 8 class ↑m
14	11, 12, 13	co 7148	. . . . . . 7 class (𝑏 ↑m 1o)
15	11, 14, 13	co 7148	. . . . . 6 class (𝑏 ↑m (𝑏 ↑m 1o))
16	10	cv 1530	. . . . . . 7 class 𝑥
17		vy	. . . . . . . 8 setvar 𝑦
18	17	cv 1530	. . . . . . . . . 10 class 𝑦
19	18	csn 4559	. . . . . . . . 9 class {𝑦}
20	12, 19	cxp 5546	. . . . . . . 8 class (1o × {𝑦})
21	17, 11, 20	cmpt 5137	. . . . . . 7 class (𝑦 ∈ 𝑏 ↦ (1o × {𝑦}))
22	16, 21	ccom 5552	. . . . . 6 class (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))
23	10, 15, 22	cmpt 5137	. . . . 5 class (𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦}))))
24	3	cv 1530	. . . . . 6 class 𝑟
25		ces 20276	. . . . . . 7 class evalSub
26	12, 5, 25	co 7148	. . . . . 6 class (1o evalSub 𝑠)
27	24, 26	cfv 6348	. . . . 5 class ((1o evalSub 𝑠)‘𝑟)
28	23, 27	ccom 5552	. . . 4 class ((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟))
29	9, 7, 28	csb 3881	. . 3 class ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟))
30	2, 3, 4, 8, 29	cmpo 7150	. 2 class (𝑠 ∈ V, 𝑟 ∈ 𝒫 (Base‘𝑠) ↦ ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))
31	1, 30	wceq 1531	1 wff evalSub1 = (𝑠 ∈ V, 𝑟 ∈ 𝒫 (Base‘𝑠) ↦ ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))

This definition is referenced by:  reldmevls1  20472  ply1frcl  20473  evls1fval  20474