Metamath Proof Explorer

Theorem evlsval

Description: Value of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 11-Mar-2015) (Revised by AV, 18-Sep-2021)

Ref Expression
Hypotheses evlsval.q 
|- Q = ( ( I evalSub S ) ` R )
evlsval.w 
|- W = ( I mPoly U )
evlsval.v 
|- V = ( I mVar U )
evlsval.u 
|- U = ( S |`s R )
evlsval.t 
|- T = ( S ^s ( B ^m I ) )
evlsval.b 
|- B = ( Base ` S )
evlsval.a 
|- A = ( algSc ` W )
evlsval.x 
|- X = ( x e. R |-> ( ( B ^m I ) X. { x } ) )
evlsval.y 
|- Y = ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) )
Assertion evlsval 
|- ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q = ( iota_ f e. ( W RingHom T ) ( ( f o. A ) = X /\ ( f o. V ) = Y ) ) )

Proof

Step Hyp Ref Expression
1 evlsval.q 
 |-  Q = ( ( I evalSub S ) ` R )
2 evlsval.w 
 |-  W = ( I mPoly U )
3 evlsval.v 
 |-  V = ( I mVar U )
4 evlsval.u 
 |-  U = ( S |`s R )
5 evlsval.t 
 |-  T = ( S ^s ( B ^m I ) )
6 evlsval.b 
 |-  B = ( Base ` S )
7 evlsval.a 
 |-  A = ( algSc ` W )
8 evlsval.x 
 |-  X = ( x e. R |-> ( ( B ^m I ) X. { x } ) )
9 evlsval.y 
 |-  Y = ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) )
10 elex 
 |-  ( I e. Z -> I e. _V )
11 fveq2 
 |-  ( s = S -> ( Base ` s ) = ( Base ` S ) )
12 11 adantl 
 |-  ( ( i = I /\ s = S ) -> ( Base ` s ) = ( Base ` S ) )
13 12 csbeq1d 
 |-  ( ( i = I /\ s = S ) -> [_ ( 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 ) ) ) ) ) ) = [_ ( 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 ) ) ) ) ) ) )
14 fvex 
 |-  ( Base ` S ) e. _V
15 14 a1i 
 |-  ( ( i = I /\ s = S ) -> ( Base ` S ) e. _V )
16 simplr 
 |-  ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) -> s = S )
17 16 fveq2d 
 |-  ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) -> ( SubRing ` s ) = ( SubRing ` S ) )
18 simpll 
 |-  ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) -> i = I )
19 oveq1 
 |-  ( s = S -> ( s |`s r ) = ( S |`s r ) )
20 19 ad2antlr 
 |-  ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) -> ( s |`s r ) = ( S |`s r ) )
21 18 20 oveq12d 
 |-  ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) -> ( i mPoly ( s |`s r ) ) = ( I mPoly ( S |`s r ) ) )
22 21 csbeq1d 
 |-  ( ( ( i = I /\ s = S ) /\ b = ( Base ` 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 ) ) ) ) ) = [_ ( 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 ) ) ) ) ) )
23 ovexd 
 |-  ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) -> ( I mPoly ( S |`s r ) ) e. _V )
24 simprr 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> w = ( I mPoly ( S |`s r ) ) )
25 simplr 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> s = S )
26 simprl 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> b = ( Base ` S ) )
27 simpll 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> i = I )
28 26 27 oveq12d 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( b ^m i ) = ( ( Base ` S ) ^m I ) )
29 25 28 oveq12d 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( s ^s ( b ^m i ) ) = ( S ^s ( ( Base ` S ) ^m I ) ) )
30 24 29 oveq12d 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( w RingHom ( s ^s ( b ^m i ) ) ) = ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) )
31 24 fveq2d 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( algSc ` w ) = ( algSc ` ( I mPoly ( S |`s r ) ) ) )
32 31 coeq2d 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( f o. ( algSc ` w ) ) = ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) )
33 28 xpeq1d 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( ( b ^m i ) X. { x } ) = ( ( ( Base ` S ) ^m I ) X. { x } ) )
34 33 mpteq2dv 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( x e. r |-> ( ( b ^m i ) X. { x } ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) )
35 32 34 eqeq12d 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( ( f o. ( algSc ` w ) ) = ( x e. r |-> ( ( b ^m i ) X. { x } ) ) <-> ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) ) )
36 25 oveq1d 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( s |`s r ) = ( S |`s r ) )
37 27 36 oveq12d 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( i mVar ( s |`s r ) ) = ( I mVar ( S |`s r ) ) )
38 37 coeq2d 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( f o. ( i mVar ( s |`s r ) ) ) = ( f o. ( I mVar ( S |`s r ) ) ) )
39 28 mpteq1d 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( g e. ( b ^m i ) |-> ( g ` x ) ) = ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) )
40 27 39 mpteq12dv 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) )
41 38 40 eqeq12d 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( ( f o. ( i mVar ( s |`s r ) ) ) = ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) ) <-> ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) )
42 35 41 anbi12d 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( ( ( 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 ) ) ) ) <-> ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) )
43 30 42 riotaeqbidv 
 |-  ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S |`s r ) ) ) ) -> ( 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 ) ) ) ) ) = ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) )
44 43 anassrs 
 |-  ( ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) /\ w = ( I mPoly ( S |`s r ) ) ) -> ( 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 ) ) ) ) ) = ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) )
45 23 44 csbied 
 |-  ( ( ( i = I /\ s = S ) /\ b = ( Base ` 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 ) ) ) ) ) = ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) )
46 22 45 eqtrd 
 |-  ( ( ( i = I /\ s = S ) /\ b = ( Base ` 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 ) ) ) ) ) = ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) )
47 17 46 mpteq12dv 
 |-  ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) -> ( 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 ) ) ) ) ) ) = ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) ) )
48 15 47 csbied 
 |-  ( ( i = I /\ s = S ) -> [_ ( 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 ) ) ) ) ) ) = ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) ) )
49 13 48 eqtrd 
 |-  ( ( i = I /\ s = S ) -> [_ ( 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 ) ) ) ) ) ) = ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) ) )
50 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 ) ) ) ) ) ) )
51 fvex 
 |-  ( SubRing ` S ) e. _V
52 51 mptex 
 |-  ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) ) e. _V
53 49 50 52 ovmpoa 
 |-  ( ( I e. _V /\ S e. CRing ) -> ( I evalSub S ) = ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) ) )
54 53 fveq1d 
 |-  ( ( I e. _V /\ S e. CRing ) -> ( ( I evalSub S ) ` R ) = ( ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) ) ` R ) )
55 10 54 sylan 
 |-  ( ( I e. Z /\ S e. CRing ) -> ( ( I evalSub S ) ` R ) = ( ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) ) ` R ) )
56 1 55 syl5eq 
 |-  ( ( I e. Z /\ S e. CRing ) -> Q = ( ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) ) ` R ) )
57 56 3adant3 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q = ( ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) ) ` R ) )
58 oveq2 
 |-  ( r = R -> ( S |`s r ) = ( S |`s R ) )
59 58 oveq2d 
 |-  ( r = R -> ( I mPoly ( S |`s r ) ) = ( I mPoly ( S |`s R ) ) )
60 59 oveq1d 
 |-  ( r = R -> ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) = ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) )
61 59 fveq2d 
 |-  ( r = R -> ( algSc ` ( I mPoly ( S |`s r ) ) ) = ( algSc ` ( I mPoly ( S |`s R ) ) ) )
62 61 coeq2d 
 |-  ( r = R -> ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( f o. ( algSc ` ( I mPoly ( S |`s R ) ) ) ) )
63 mpteq1 
 |-  ( r = R -> ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) )
64 62 63 eqeq12d 
 |-  ( r = R -> ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) <-> ( f o. ( algSc ` ( I mPoly ( S |`s R ) ) ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) ) )
65 58 oveq2d 
 |-  ( r = R -> ( I mVar ( S |`s r ) ) = ( I mVar ( S |`s R ) ) )
66 65 coeq2d 
 |-  ( r = R -> ( f o. ( I mVar ( S |`s r ) ) ) = ( f o. ( I mVar ( S |`s R ) ) ) )
67 66 eqeq1d 
 |-  ( r = R -> ( ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) <-> ( f o. ( I mVar ( S |`s R ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) )
68 64 67 anbi12d 
 |-  ( r = R -> ( ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) <-> ( ( f o. ( algSc ` ( I mPoly ( S |`s R ) ) ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s R ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) )
69 60 68 riotaeqbidv 
 |-  ( r = R -> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) = ( iota_ f e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s R ) ) ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s R ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) )
70 eqid 
 |-  ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) ) = ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) )
71 riotaex 
 |-  ( iota_ f e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s R ) ) ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s R ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) e. _V
72 69 70 71 fvmpt 
 |-  ( R e. ( SubRing ` S ) -> ( ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) ) ` R ) = ( iota_ f e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s R ) ) ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s R ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) )
73 4 oveq2i 
 |-  ( I mPoly U ) = ( I mPoly ( S |`s R ) )
74 2 73 eqtri 
 |-  W = ( I mPoly ( S |`s R ) )
75 6 oveq1i 
 |-  ( B ^m I ) = ( ( Base ` S ) ^m I )
76 75 oveq2i 
 |-  ( S ^s ( B ^m I ) ) = ( S ^s ( ( Base ` S ) ^m I ) )
77 5 76 eqtri 
 |-  T = ( S ^s ( ( Base ` S ) ^m I ) )
78 74 77 oveq12i 
 |-  ( W RingHom T ) = ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) )
79 78 a1i 
 |-  ( T. -> ( W RingHom T ) = ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) )
80 74 fveq2i 
 |-  ( algSc ` W ) = ( algSc ` ( I mPoly ( S |`s R ) ) )
81 7 80 eqtri 
 |-  A = ( algSc ` ( I mPoly ( S |`s R ) ) )
82 81 coeq2i 
 |-  ( f o. A ) = ( f o. ( algSc ` ( I mPoly ( S |`s R ) ) ) )
83 75 xpeq1i 
 |-  ( ( B ^m I ) X. { x } ) = ( ( ( Base ` S ) ^m I ) X. { x } )
84 83 mpteq2i 
 |-  ( x e. R |-> ( ( B ^m I ) X. { x } ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) )
85 8 84 eqtri 
 |-  X = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) )
86 82 85 eqeq12i 
 |-  ( ( f o. A ) = X <-> ( f o. ( algSc ` ( I mPoly ( S |`s R ) ) ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) )
87 4 oveq2i 
 |-  ( I mVar U ) = ( I mVar ( S |`s R ) )
88 3 87 eqtri 
 |-  V = ( I mVar ( S |`s R ) )
89 88 coeq2i 
 |-  ( f o. V ) = ( f o. ( I mVar ( S |`s R ) ) )
90 eqid 
 |-  ( g ` x ) = ( g ` x )
91 75 90 mpteq12i 
 |-  ( g e. ( B ^m I ) |-> ( g ` x ) ) = ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) )
92 91 mpteq2i 
 |-  ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) )
93 9 92 eqtri 
 |-  Y = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) )
94 89 93 eqeq12i 
 |-  ( ( f o. V ) = Y <-> ( f o. ( I mVar ( S |`s R ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) )
95 86 94 anbi12i 
 |-  ( ( ( f o. A ) = X /\ ( f o. V ) = Y ) <-> ( ( f o. ( algSc ` ( I mPoly ( S |`s R ) ) ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s R ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) )
96 95 a1i 
 |-  ( T. -> ( ( ( f o. A ) = X /\ ( f o. V ) = Y ) <-> ( ( f o. ( algSc ` ( I mPoly ( S |`s R ) ) ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s R ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) )
97 79 96 riotaeqbidv 
 |-  ( T. -> ( iota_ f e. ( W RingHom T ) ( ( f o. A ) = X /\ ( f o. V ) = Y ) ) = ( iota_ f e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s R ) ) ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s R ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) )
98 97 mptru 
 |-  ( iota_ f e. ( W RingHom T ) ( ( f o. A ) = X /\ ( f o. V ) = Y ) ) = ( iota_ f e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s R ) ) ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s R ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) )
99 72 98 eqtr4di 
 |-  ( R e. ( SubRing ` S ) -> ( ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) ) ` R ) = ( iota_ f e. ( W RingHom T ) ( ( f o. A ) = X /\ ( f o. V ) = Y ) ) )
100 99 3ad2ant3 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( r e. ( SubRing ` S ) |-> ( iota_ f e. ( ( I mPoly ( S |`s r ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) ( ( f o. ( algSc ` ( I mPoly ( S |`s r ) ) ) ) = ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) /\ ( f o. ( I mVar ( S |`s r ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) ) ) ) ` R ) = ( iota_ f e. ( W RingHom T ) ( ( f o. A ) = X /\ ( f o. V ) = Y ) ) )
101 57 100 eqtrd 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q = ( iota_ f e. ( W RingHom T ) ( ( f o. A ) = X /\ ( f o. V ) = Y ) ) )