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 \in V ⟼ ⦋ {Base}_{r} / b ⦌ ((x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (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_{𝑜} \times \{y\})$
18	14 8 17	cmpt	$class (y \in b ⟼ 1_{𝑜} \times \{y\})$
19	13 18	ccom	$class (x \circ (y \in b ⟼ 1_{𝑜} \times \{y\}))$
20	7 12 19	cmpt	$class (x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\}))$
21		cevl	$class eval$
22	10 4 21	co	$class (1_{𝑜} eval r)$
23	20 22	ccom	$class ((x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} eval r))$
24	6 5 23	csb	$class ⦋ {Base}_{r} / b ⦌ ((x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} eval r))$
25	1 2 24	cmpt	$class (r \in V ⟼ ⦋ {Base}_{r} / b ⦌ ((x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} eval r)))$
26	0 25	wceq	$wff {eval}_{1} = (r \in V ⟼ ⦋ {Base}_{r} / b ⦌ ((x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} eval r)))$

Metamath Proof Explorer

Definition df-evl1

Detailed syntax breakdown