Metamath Proof Explorer

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