Metamath Proof Explorer


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 𝑟 ) ) )