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 ⊢ eval 1 = r ∈ V ⟼ ⦋ Base r / b⦌ x ∈ b b 1 𝑜 ⟼ x ∘ y ∈ b ⟼ 1 𝑜 × y ∘ 1 𝑜 eval r

Detailed syntax breakdown

Step Hyp Ref Expression
0 ce1 class eval 1
1 vr setvar r
2 cvv class V
3 cbs class Base
4 1 cv setvar r
5 4 3 cfv class Base r
6 vb setvar b
7 vx setvar x
8 6 cv setvar b
9 cmap class ↑ 𝑚
10 c1o class 1 𝑜
11 8 10 9 co class b 1 𝑜
12 8 11 9 co class b b 1 𝑜
13 7 cv setvar x
14 vy setvar y
15 14 cv setvar y
16 15 csn class y
17 10 16 cxp class 1 𝑜 × y
18 14 8 17 cmpt class y ∈ b ⟼ 1 𝑜 × y
19 13 18 ccom class x ∘ y ∈ b ⟼ 1 𝑜 × y
20 7 12 19 cmpt class x ∈ b b 1 𝑜 ⟼ x ∘ y ∈ b ⟼ 1 𝑜 × y
21 cevl class eval
22 10 4 21 co class 1 𝑜 eval r
23 20 22 ccom class x ∈ b b 1 𝑜 ⟼ x ∘ y ∈ b ⟼ 1 𝑜 × y ∘ 1 𝑜 eval r
24 6 5 23 csb class ⦋ Base r / b⦌ x ∈ b b 1 𝑜 ⟼ x ∘ y ∈ b ⟼ 1 𝑜 × y ∘ 1 𝑜 eval r
25 1 2 24 cmpt class r ∈ V ⟼ ⦋ Base r / b⦌ x ∈ b b 1 𝑜 ⟼ x ∘ y ∈ b ⟼ 1 𝑜 × y ∘ 1 𝑜 eval r
26 0 25 wceq wff eval 1 = r ∈ V ⟼ ⦋ Base r / b⦌ x ∈ b b 1 𝑜 ⟼ x ∘ y ∈ b ⟼ 1 𝑜 × y ∘ 1 𝑜 eval r