df-evls

Description: Define the evaluation map for the polynomial algebra. The function ( ( I evalSub S )R ) : V --> ( S ^m ( S ^m I ) ) makes sense when I is an index set, S is a ring, R is a subring of S , and where V is the set of polynomials in ( I mPoly R ) . This function maps an element of the formal polynomial algebra (with coefficients in R ) to a function from assignments I --> S of the variables to elements of S formed by evaluating the polynomial with the given assignments. (Contributed by Stefan O'Rear, 11-Mar-2015)

		Ref	Expression
	Assertion	df-evls	$⊢ evalSub = (i \in V, s \in CRing ⟼ ⦋ {Base}_{s} / b ⦌ (r \in SubRing (s) ⟼ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ces	$class evalSub$
1		vi	$setvar i$
2		cvv	$class V$
3		vs	$setvar s$
4		ccrg	$class CRing$
5		cbs	$class Base$
6	3	cv	$setvar s$
7	6 5	cfv	$class {Base}_{s}$
8		vb	$setvar b$
9		vr	$setvar r$
10		csubrg	$class SubRing$
11	6 10	cfv	$class SubRing (s)$
12	1	cv	$setvar i$
13		cmpl	$class mPoly$
14		cress	$class ↾_{𝑠}$
15	9	cv	$setvar r$
16	6 15 14	co	$class (s ↾_{𝑠} r)$
17	12 16 13	co	$class (i mPoly (s ↾_{𝑠} r))$
18		vw	$setvar w$
19		vf	$setvar f$
20	18	cv	$setvar w$
21		crh	$class RingHom$
22		cpws	$class ↑_{𝑠}$
23	8	cv	$setvar b$
24		cmap	$class ↑_{𝑚}$
25	23 12 24	co	$class (b^{i})$
26	6 25 22	co	$class (s ↑_{𝑠} (b^{i}))$
27	20 26 21	co	$class (w RingHom (s ↑_{𝑠} (b^{i})))$
28	19	cv	$setvar f$
29		cascl	$class algSc$
30	20 29	cfv	$class algSc (w)$
31	28 30	ccom	$class (f \circ algSc (w))$
32		vx	$setvar x$
33	32	cv	$setvar x$
34	33	csn	$class \{x\}$
35	25 34	cxp	$class ((b^{i}) \times \{x\})$
36	32 15 35	cmpt	$class (x \in r ⟼ (b^{i}) \times \{x\})$
37	31 36	wceq	$wff f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\})$
38		cmvr	$class mVar$
39	12 16 38	co	$class (i mVar (s ↾_{𝑠} r))$
40	28 39	ccom	$class (f \circ (i mVar (s ↾_{𝑠} r)))$
41		vg	$setvar g$
42	41	cv	$setvar g$
43	33 42	cfv	$class g (x)$
44	41 25 43	cmpt	$class (g \in (b^{i}) ⟼ g (x))$
45	32 12 44	cmpt	$class (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))$
46	40 45	wceq	$wff f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))$
47	37 46	wa	$wff (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))$
48	47 19 27	crio	$class (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))$
49	18 17 48	csb	$class ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))$
50	9 11 49	cmpt	$class (r \in SubRing (s) ⟼ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))))$
51	8 7 50	csb	$class ⦋ {Base}_{s} / b ⦌ (r \in SubRing (s) ⟼ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))))$
52	1 3 2 4 51	cmpo	$class (i \in V, s \in CRing ⟼ ⦋ {Base}_{s} / b ⦌ (r \in SubRing (s) ⟼ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))))$
53	0 52	wceq	$wff evalSub = (i \in V, s \in CRing ⟼ ⦋ {Base}_{s} / b ⦌ (r \in SubRing (s) ⟼ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))))$

Metamath Proof Explorer

Definition df-evls

Detailed syntax breakdown