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

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