Metamath Proof Explorer

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 ces 
 |-  evalSub
1 vi 
 |-  i
2 cvv 
 |-  _V
3 vs 
 |-  s
4 ccrg 
 |-  CRing
5 cbs 
 |-  Base
6 3 cv 
 |-  s
7 6 5 cfv 
 |-  ( Base ` s )
8 vb 
 |-  b
9 vr 
 |-  r
10 csubrg 
 |-  SubRing
11 6 10 cfv 
 |-  ( SubRing ` s )
12 1 cv 
 |-  i
13 cmpl 
 |-  mPoly
14 cress 
 |-  |`s
15 9 cv 
 |-  r
16 6 15 14 co 
 |-  ( s |`s r )
17 12 16 13 co 
 |-  ( i mPoly ( s |`s r ) )
18 vw 
 |-  w
19 vf 
 |-  f
20 18 cv 
 |-  w
21 crh 
 |-  RingHom
22 cpws 
 |-  ^s
23 8 cv 
 |-  b
24 cmap 
 |-  ^m
25 23 12 24 co 
 |-  ( b ^m i )
26 6 25 22 co 
 |-  ( s ^s ( b ^m i ) )
27 20 26 21 co 
 |-  ( w RingHom ( s ^s ( b ^m i ) ) )
28 19 cv 
 |-  f
29 cascl 
 |-  algSc
30 20 29 cfv 
 |-  ( algSc ` w )
31 28 30 ccom 
 |-  ( f o. ( algSc ` w ) )
32 vx 
 |-  x
33 32 cv 
 |-  x
34 33 csn 
 |-  { x }
35 25 34 cxp 
 |-  ( ( b ^m i ) X. { x } )
36 32 15 35 cmpt 
 |-  ( x e. r |-> ( ( b ^m i ) X. { x } ) )
37 31 36 wceq 
 |-  ( f o. ( algSc ` w ) ) = ( x e. r |-> ( ( b ^m i ) X. { x } ) )
38 cmvr 
 |-  mVar
39 12 16 38 co 
 |-  ( i mVar ( s |`s r ) )
40 28 39 ccom 
 |-  ( f o. ( i mVar ( s |`s r ) ) )
41 vg 
 |-  g
42 41 cv 
 |-  g
43 33 42 cfv 
 |-  ( g ` x )
44 41 25 43 cmpt 
 |-  ( g e. ( b ^m i ) |-> ( g ` x ) )
45 32 12 44 cmpt 
 |-  ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) )
46 40 45 wceq 
 |-  ( f o. ( i mVar ( s |`s r ) ) ) = ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) )
47 37 46 wa 
 |-  ( ( 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 ) ) ) )
48 47 19 27 crio 
 |-  ( 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 ) ) ) ) )
49 18 17 48 csb 
 |-  [_ ( 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 ) ) ) ) )
50 9 11 49 cmpt 
 |-  ( 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 ) ) ) ) ) )
51 8 7 50 csb 
 |-  [_ ( 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 ) ) ) ) ) )
52 1 3 2 4 51 cmpo 
 |-  ( 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 ) ) ) ) ) ) )
53 0 52 wceq 
 |-  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 ) ) ) ) ) ) )