Definition df-evl1

Description: Define the evaluation map for the univariate polynomial algebra. The function ( eval1R ) : V --> ( R ^m R ) makes sense when R is a ring, and 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 R into an element of R formed by evaluating the polynomial with the given assignment. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Assertion	df-evl1	⊢ eval1 = ( 𝑟 ∈ V ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑟 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ce1	⊢ eval1
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		cbs	⊢ Base
4	1	cv	⊢ 𝑟
5	4 3	cfv	⊢ ( Base ‘ 𝑟 )
6		vb	⊢ 𝑏
7		vx	⊢ 𝑥
8	6	cv	⊢ 𝑏
9		cmap	⊢ ↑m
10		c1o	⊢ 1o
11	8 10 9	co	⊢ ( 𝑏 ↑m 1o )
12	8 11 9	co	⊢ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) )
13	7	cv	⊢ 𝑥
14		vy	⊢ 𝑦
15	14	cv	⊢ 𝑦
16	15	csn	⊢ { 𝑦 }
17	10 16	cxp	⊢ ( 1o × { 𝑦 } )
18	14 8 17	cmpt	⊢ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) )
19	13 18	ccom	⊢ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) )
20	7 12 19	cmpt	⊢ ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) )
21		cevl	⊢ eval
22	10 4 21	co	⊢ ( 1o eval 𝑟 )
23	20 22	ccom	⊢ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑟 ) )
24	6 5 23	csb	⊢ ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑟 ) )
25	1 2 24	cmpt	⊢ ( 𝑟 ∈ V ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑟 ) ) )
26	0 25	wceq	⊢ eval1 = ( 𝑟 ∈ V ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑟 ) ) )