Definition df-evls1

Description: Define the evaluation map for the univariate polynomial algebra. The function ( S evalSub1 R ) : V --> ( S ^m S ) makes sense when S is a ring and R is a subring of S , and where V is the set of polynomials in ( Poly1R ) . This function maps an element of the formal polynomial algebra (with coefficients in R ) to a function from assignments to the variable from S into an element of S formed by evaluating the polynomial with the given assignment. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Assertion	df-evls1	⊢ evalSub1 = ( 𝑠 ∈ V , 𝑟 ∈ 𝒫 ( Base ‘ 𝑠 ) ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ces1	⊢ evalSub1
1		vs	⊢ 𝑠
2		cvv	⊢ V
3		vr	⊢ 𝑟
4		cbs	⊢ Base
5	1	cv	⊢ 𝑠
6	5 4	cfv	⊢ ( Base ‘ 𝑠 )
7	6	cpw	⊢ 𝒫 ( Base ‘ 𝑠 )
8		vb	⊢ 𝑏
9		vx	⊢ 𝑥
10	8	cv	⊢ 𝑏
11		cmap	⊢ ↑m
12		c1o	⊢ 1o
13	10 12 11	co	⊢ ( 𝑏 ↑m 1o )
14	10 13 11	co	⊢ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) )
15	9	cv	⊢ 𝑥
16		vy	⊢ 𝑦
17	16	cv	⊢ 𝑦
18	17	csn	⊢ { 𝑦 }
19	12 18	cxp	⊢ ( 1o × { 𝑦 } )
20	16 10 19	cmpt	⊢ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) )
21	15 20	ccom	⊢ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) )
22	9 14 21	cmpt	⊢ ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) )
23		ces	⊢ evalSub
24	12 5 23	co	⊢ ( 1o evalSub 𝑠 )
25	3	cv	⊢ 𝑟
26	25 24	cfv	⊢ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 )
27	22 26	ccom	⊢ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) )
28	8 6 27	csb	⊢ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) )
29	1 3 2 7 28	cmpo	⊢ ( 𝑠 ∈ V , 𝑟 ∈ 𝒫 ( Base ‘ 𝑠 ) ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) )
30	0 29	wceq	⊢ evalSub1 = ( 𝑠 ∈ V , 𝑟 ∈ 𝒫 ( Base ‘ 𝑠 ) ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) )