Definition df-evls 19506

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

Assertion

Ref	Expression
df-evls	|- evalSub = ( i e. _V , s e. CRing |-> [_ ( Base ` s ) / b ]_ ( r e. (SubRing ` s ) |-> [_ ( i mPoly ( s ↾s r ) ) / w ]_ ( iota_ f e. ( w RingHom ( s ^s ( b ^m i ) ) ) ( ( f o. (algSc ` w ) ) = ( x e. r |-> ( ( b ^m i ) X. { x } ) ) /\ ( f o. ( i mVar ( s ↾s r ) ) ) = ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) ) ) ) ) )

Distinct variable group:   f, b, g, i, r, s, w, x

Detailed syntax breakdown of Definition df-evls

Step	Hyp	Ref	Expression
1		ces 19504	. 2 class evalSub
2		vi	. . 3 setvar i
3		vs	. . 3 setvar s
4		cvv 3200	. . 3 class _V
5		ccrg 18548	. . 3 class CRing
6		vb	. . . 4 setvar b
7	3	cv 1482	. . . . 5 class s
8		cbs 15857	. . . . 5 class Base
9	7, 8	cfv 5888	. . . 4 class ( Base ` s )
10		vr	. . . . 5 setvar r
11		csubrg 18776	. . . . . 6 class SubRing
12	7, 11	cfv 5888	. . . . 5 class (SubRing ` s )
13		vw	. . . . . 6 setvar w
14	2	cv 1482	. . . . . . 7 class i
15	10	cv 1482	. . . . . . . 8 class r
16		cress 15858	. . . . . . . 8 class ↾s
17	7, 15, 16	co 6650	. . . . . . 7 class ( s ↾s r )
18		cmpl 19353	. . . . . . 7 class mPoly
19	14, 17, 18	co 6650	. . . . . 6 class ( i mPoly ( s ↾s r ) )
20		vf	. . . . . . . . . . 11 setvar f
21	20	cv 1482	. . . . . . . . . 10 class f
22	13	cv 1482	. . . . . . . . . . 11 class w
23		cascl 19311	. . . . . . . . . . 11 class algSc
24	22, 23	cfv 5888	. . . . . . . . . 10 class (algSc ` w )
25	21, 24	ccom 5118	. . . . . . . . 9 class ( f o. (algSc ` w ) )
26		vx	. . . . . . . . . 10 setvar x
27	6	cv 1482	. . . . . . . . . . . 12 class b
28		cmap 7857	. . . . . . . . . . . 12 class ^m
29	27, 14, 28	co 6650	. . . . . . . . . . 11 class ( b ^m i )
30	26	cv 1482	. . . . . . . . . . . 12 class x
31	30	csn 4177	. . . . . . . . . . 11 class { x }
32	29, 31	cxp 5112	. . . . . . . . . 10 class ( ( b ^m i ) X. { x } )
33	26, 15, 32	cmpt 4729	. . . . . . . . 9 class ( x e. r |-> ( ( b ^m i ) X. { x } ) )
34	25, 33	wceq 1483	. . . . . . . 8 wff ( f o. (algSc ` w ) ) = ( x e. r |-> ( ( b ^m i ) X. { x } ) )
35		cmvr 19352	. . . . . . . . . . 11 class mVar
36	14, 17, 35	co 6650	. . . . . . . . . 10 class ( i mVar ( s ↾s r ) )
37	21, 36	ccom 5118	. . . . . . . . 9 class ( f o. ( i mVar ( s ↾s r ) ) )
38		vg	. . . . . . . . . . 11 setvar g
39	38	cv 1482	. . . . . . . . . . . 12 class g
40	30, 39	cfv 5888	. . . . . . . . . . 11 class ( g ` x )
41	38, 29, 40	cmpt 4729	. . . . . . . . . 10 class ( g e. ( b ^m i ) |-> ( g ` x ) )
42	26, 14, 41	cmpt 4729	. . . . . . . . 9 class ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) )
43	37, 42	wceq 1483	. . . . . . . 8 wff ( f o. ( i mVar ( s ↾s r ) ) ) = ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) )
44	34, 43	wa 384	. . . . . . 7 wff ( ( f o. (algSc ` w ) ) = ( x e. r |-> ( ( b ^m i ) X. { x } ) ) /\ ( f o. ( i mVar ( s ↾s r ) ) ) = ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) ) )
45		cpws 16107	. . . . . . . . 9 class ^s
46	7, 29, 45	co 6650	. . . . . . . 8 class ( s ^s ( b ^m i ) )
47		crh 18712	. . . . . . . 8 class RingHom
48	22, 46, 47	co 6650	. . . . . . 7 class ( w RingHom ( s ^s ( b ^m i ) ) )
49	44, 20, 48	crio 6610	. . . . . 6 class ( iota_ f e. ( w RingHom ( s ^s ( b ^m i ) ) ) ( ( f o. (algSc ` w ) ) = ( x e. r |-> ( ( b ^m i ) X. { x } ) ) /\ ( f o. ( i mVar ( s ↾s r ) ) ) = ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) ) ) )
50	13, 19, 49	csb 3533	. . . . 5 class [_ ( i mPoly ( s ↾s r ) ) / w ]_ ( iota_ f e. ( w RingHom ( s ^s ( b ^m i ) ) ) ( ( f o. (algSc ` w ) ) = ( x e. r |-> ( ( b ^m i ) X. { x } ) ) /\ ( f o. ( i mVar ( s ↾s r ) ) ) = ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) ) ) )
51	10, 12, 50	cmpt 4729	. . . 4 class ( r e. (SubRing ` s ) |-> [_ ( i mPoly ( s ↾s r ) ) / w ]_ ( iota_ f e. ( w RingHom ( s ^s ( b ^m i ) ) ) ( ( f o. (algSc ` w ) ) = ( x e. r |-> ( ( b ^m i ) X. { x } ) ) /\ ( f o. ( i mVar ( s ↾s r ) ) ) = ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) ) ) ) )
52	6, 9, 51	csb 3533	. . 3 class [_ ( Base ` s ) / b ]_ ( r e. (SubRing ` s ) |-> [_ ( i mPoly ( s ↾s r ) ) / w ]_ ( iota_ f e. ( w RingHom ( s ^s ( b ^m i ) ) ) ( ( f o. (algSc ` w ) ) = ( x e. r |-> ( ( b ^m i ) X. { x } ) ) /\ ( f o. ( i mVar ( s ↾s r ) ) ) = ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) ) ) ) )
53	2, 3, 4, 5, 52	cmpt2 6652	. 2 class ( i e. _V , s e. CRing |-> [_ ( Base ` s ) / b ]_ ( r e. (SubRing ` s ) |-> [_ ( i mPoly ( s ↾s r ) ) / w ]_ ( iota_ f e. ( w RingHom ( s ^s ( b ^m i ) ) ) ( ( f o. (algSc ` w ) ) = ( x e. r |-> ( ( b ^m i ) X. { x } ) ) /\ ( f o. ( i mVar ( s ↾s r ) ) ) = ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) ) ) ) ) )
54	1, 53	wceq 1483	1 wff evalSub = ( i e. _V , s e. CRing |-> [_ ( Base ` s ) / b ]_ ( r e. (SubRing ` s ) |-> [_ ( i mPoly ( s ↾s r ) ) / w ]_ ( iota_ f e. ( w RingHom ( s ^s ( b ^m i ) ) ) ( ( f o. (algSc ` w ) ) = ( x e. r |-> ( ( b ^m i ) X. { x } ) ) /\ ( f o. ( i mVar ( s ↾s r ) ) ) = ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) ) ) ) ) )

This definition is referenced by:  reldmevls  19517  mpfrcl  19518  evlsval  19519