This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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