Definition df-evls1 22319

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 22317	. 2 class evalSub1
2		vs	. . 3 setvar 𝑠
3		vr	. . 3 setvar 𝑟
4		cvv 3480	. . 3 class V
5	2	cv 1539	. . . . 5 class 𝑠
6		cbs 17247	. . . . 5 class Base
7	5, 6	cfv 6561	. . . 4 class (Base‘𝑠)
8	7	cpw 4600	. . 3 class 𝒫 (Base‘𝑠)
9		vb	. . . 4 setvar 𝑏
10		vx	. . . . . 6 setvar 𝑥
11	9	cv 1539	. . . . . . 7 class 𝑏
12		c1o 8499	. . . . . . . 8 class 1o
13		cmap 8866	. . . . . . . 8 class ↑m
14	11, 12, 13	co 7431	. . . . . . 7 class (𝑏 ↑m 1o)
15	11, 14, 13	co 7431	. . . . . 6 class (𝑏 ↑m (𝑏 ↑m 1o))
16	10	cv 1539	. . . . . . 7 class 𝑥
17		vy	. . . . . . . 8 setvar 𝑦
18	17	cv 1539	. . . . . . . . . 10 class 𝑦
19	18	csn 4626	. . . . . . . . 9 class {𝑦}
20	12, 19	cxp 5683	. . . . . . . 8 class (1o × {𝑦})
21	17, 11, 20	cmpt 5225	. . . . . . 7 class (𝑦 ∈ 𝑏 ↦ (1o × {𝑦}))
22	16, 21	ccom 5689	. . . . . 6 class (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))
23	10, 15, 22	cmpt 5225	. . . . 5 class (𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦}))))
24	3	cv 1539	. . . . . 6 class 𝑟
25		ces 22096	. . . . . . 7 class evalSub
26	12, 5, 25	co 7431	. . . . . 6 class (1o evalSub 𝑠)
27	24, 26	cfv 6561	. . . . 5 class ((1o evalSub 𝑠)‘𝑟)
28	23, 27	ccom 5689	. . . 4 class ((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟))
29	9, 7, 28	csb 3899	. . 3 class ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟))
30	2, 3, 4, 8, 29	cmpo 7433	. 2 class (𝑠 ∈ V, 𝑟 ∈ 𝒫 (Base‘𝑠) ↦ ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))
31	1, 30	wceq 1540	1 wff evalSub1 = (𝑠 ∈ V, 𝑟 ∈ 𝒫 (Base‘𝑠) ↦ ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))

This definition is referenced by:  reldmevls1  22321  ply1frcl  22322  evls1fval  22323