Theorem evlsval 19897

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

Hypotheses

Ref	Expression
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

Ref	Expression
evlsval	|- ( ( I e. _V /\ S e. CRing /\ R e. (SubRing ` S ) ) -> Q = ( iota_ f e. ( W RingHom T ) ( ( f o. A ) = X /\ ( f o. V ) = Y ) ) )

Distinct variable groups:   f, I, g, x   R, f, x   S, f, g, x   T, f   f, W

Allowed substitution hints:   A( x, f, g)   B( x, f, g)   Q( x, f, g)   R( g)   T( x, g)   U( x, f, g)   V( x, f, g)   W( x, g)   X( x, f, g)   Y( x, f, g)

Proof of Theorem evlsval

Dummy variables b i r s w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		evlsval.q	. . . 4 |- Q = ( ( I evalSub S ) ` R )
2		fveq2 5691	. . . . . . . . 9 |- ( s = S -> ( Base ` s ) = ( Base ` S ) )
3	2	adantl 453	. . . . . . . 8 |- ( ( i = I /\ s = S ) -> ( Base ` s ) = ( Base ` S ) )
4	3	csbeq1d 3221	. . . . . . 7 |- ( ( 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 ) ) ) ) ) ) )
5		fvex 5705	. . . . . . . . 9 |- ( Base ` S ) e. _V
6	5	a1i 11	. . . . . . . 8 |- ( ( i = I /\ s = S ) -> ( Base ` S ) e. _V )
7		simplr 732	. . . . . . . . . 10 |- ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) -> s = S )
8	7	fveq2d 5695	. . . . . . . . 9 |- ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) -> (SubRing ` s ) = (SubRing ` S ) )
9		simpll 731	. . . . . . . . . . . 12 |- ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) -> i = I )
10		oveq1 6051	. . . . . . . . . . . . 13 |- ( s = S -> ( s ↾s r ) = ( S ↾s r ) )
11	10	ad2antlr 708	. . . . . . . . . . . 12 |- ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) -> ( s ↾s r ) = ( S ↾s r ) )
12	9, 11	oveq12d 6062	. . . . . . . . . . 11 |- ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) -> ( i mPoly ( s ↾s r ) ) = ( I mPoly ( S ↾s r ) ) )
13	12	csbeq1d 3221	. . . . . . . . . 10 |- ( ( ( 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 ) ) ) ) ) )
14		ovex 6069	. . . . . . . . . . . 12 |- ( I mPoly ( S ↾s r ) ) e. _V
15	14	a1i 11	. . . . . . . . . . 11 |- ( ( ( i = I /\ s = S ) /\ b = ( Base ` S ) ) -> ( I mPoly ( S ↾s r ) ) e. _V )
16		simprr 734	. . . . . . . . . . . . . 14 |- ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S ↾s r ) ) ) ) -> w = ( I mPoly ( S ↾s r ) ) )
17		simplr 732	. . . . . . . . . . . . . . 15 |- ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S ↾s r ) ) ) ) -> s = S )
18		simprl 733	. . . . . . . . . . . . . . . 16 |- ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S ↾s r ) ) ) ) -> b = ( Base ` S ) )
19		simpll 731	. . . . . . . . . . . . . . . 16 |- ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S ↾s r ) ) ) ) -> i = I )
20	18, 19	oveq12d 6062	. . . . . . . . . . . . . . 15 |- ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S ↾s r ) ) ) ) -> ( b ^m i ) = ( ( Base ` S ) ^m I ) )
21	17, 20	oveq12d 6062	. . . . . . . . . . . . . 14 |- ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S ↾s r ) ) ) ) -> ( s ^s ( b ^m i ) ) = ( S ^s ( ( Base ` S ) ^m I ) ) )
22	16, 21	oveq12d 6062	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) ) )
23	16	fveq2d 5695	. . . . . . . . . . . . . . . 16 |- ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S ↾s r ) ) ) ) -> (algSc ` w ) = (algSc ` ( I mPoly ( S ↾s r ) ) ) )
24	23	coeq2d 4998	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) ) ) )
25	20	xpeq1d 4864	. . . . . . . . . . . . . . . 16 |- ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S ↾s r ) ) ) ) -> ( ( b ^m i ) X. { x } ) = ( ( ( Base ` S ) ^m I ) X. { x } ) )
26	25	mpteq2dv 4260	. . . . . . . . . . . . . . 15 |- ( ( ( 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 } ) ) )
27	24, 26	eqeq12d 2422	. . . . . . . . . . . . . 14 |- ( ( ( 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 } ) ) ) )
28	17	oveq1d 6059	. . . . . . . . . . . . . . . . 17 |- ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S ↾s r ) ) ) ) -> ( s ↾s r ) = ( S ↾s r ) )
29	19, 28	oveq12d 6062	. . . . . . . . . . . . . . . 16 |- ( ( ( i = I /\ s = S ) /\ ( b = ( Base ` S ) /\ w = ( I mPoly ( S ↾s r ) ) ) ) -> ( i mVar ( s ↾s r ) ) = ( I mVar ( S ↾s r ) ) )
30	29	coeq2d 4998	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) ) )
31	20	mpteq1d 4254	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) ) )
32	19, 31	mpteq12dv 4251	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) ) )
33	30, 32	eqeq12d 2422	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) ) ) )
34	27, 33	anbi12d 692	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) ) ) ) )
35	22, 34	riotaeqbidv 6515	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) ) ) ) )
36	35	anassrs 630	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) ) ) ) )
37	15, 36	csbied 3257	. . . . . . . . . 10 |- ( ( ( 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 ) ) ) ) ) )
38	13, 37	eqtrd 2440	. . . . . . . . 9 |- ( ( ( 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 ) ) ) ) ) )
39	8, 38	mpteq12dv 4251	. . . . . . . 8 |- ( ( ( 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 ) ) ) ) ) ) )
40	6, 39	csbied 3257	. . . . . . 7 |- ( ( 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 ) ) ) ) ) ) )
41	4, 40	eqtrd 2440	. . . . . 6 |- ( ( 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 ) ) ) ) ) ) )
42		df-evls 16379	. . . . . 6 |- 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 ) ) ) ) ) ) )
43		fvex 5705	. . . . . . 7 |- (SubRing ` S ) e. _V
44	43	mptex 5929	. . . . . 6 |- ( 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
45	41, 42, 44	ovmpt2a 6167	. . . . 5 |- ( ( 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 ) ) ) ) ) ) )
46	45	fveq1d 5693	. . . 4 |- ( ( 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 ) )
47	1, 46	syl5eq 2452	. . 3 |- ( ( I e. _V /\ 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 ) )
48	47	3adant3 977	. 2 |- ( ( I e. _V /\ 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 ) )
49		oveq2 6052	. . . . . . . 8 |- ( r = R -> ( S ↾s r ) = ( S ↾s R ) )
50	49	oveq2d 6060	. . . . . . 7 |- ( r = R -> ( I mPoly ( S ↾s r ) ) = ( I mPoly ( S ↾s R ) ) )
51	50	oveq1d 6059	. . . . . 6 |- ( 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 ) ) ) )
52	50	fveq2d 5695	. . . . . . . . 9 |- ( r = R -> (algSc ` ( I mPoly ( S ↾s r ) ) ) = (algSc ` ( I mPoly ( S ↾s R ) ) ) )
53	52	coeq2d 4998	. . . . . . . 8 |- ( r = R -> ( f o. (algSc ` ( I mPoly ( S ↾s r ) ) ) ) = ( f o. (algSc ` ( I mPoly ( S ↾s R ) ) ) ) )
54		mpteq1 4253	. . . . . . . 8 |- ( r = R -> ( x e. r |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) )
55	53, 54	eqeq12d 2422	. . . . . . 7 |- ( 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 } ) ) ) )
56	49	oveq2d 6060	. . . . . . . . 9 |- ( r = R -> ( I mVar ( S ↾s r ) ) = ( I mVar ( S ↾s R ) ) )
57	56	coeq2d 4998	. . . . . . . 8 |- ( r = R -> ( f o. ( I mVar ( S ↾s r ) ) ) = ( f o. ( I mVar ( S ↾s R ) ) ) )
58	57	eqeq1d 2416	. . . . . . 7 |- ( 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 ) ) ) ) )
59	55, 58	anbi12d 692	. . . . . 6 |- ( 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 ) ) ) ) ) )
60	51, 59	riotaeqbidv 6515	. . . . 5 |- ( 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 ) ) ) ) ) )
61		eqid 2408	. . . . 5 |- ( 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 ) ) ) ) ) )
62		riotaex 6516	. . . . 5 |- ( 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
63	60, 61, 62	fvmpt 5769	. . . 4 |- ( 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 ) ) ) ) ) )
64		evlsval.w	. . . . . . . . 9 |- W = ( I mPoly U )
65		evlsval.u	. . . . . . . . . 10 |- U = ( S ↾s R )
66	65	oveq2i 6055	. . . . . . . . 9 |- ( I mPoly U ) = ( I mPoly ( S ↾s R ) )
67	64, 66	eqtri 2428	. . . . . . . 8 |- W = ( I mPoly ( S ↾s R ) )
68		evlsval.t	. . . . . . . . 9 |- T = ( S ^s ( B ^m I ) )
69		evlsval.b	. . . . . . . . . . 11 |- B = ( Base ` S )
70	69	oveq1i 6054	. . . . . . . . . 10 |- ( B ^m I ) = ( ( Base ` S ) ^m I )
71	70	oveq2i 6055	. . . . . . . . 9 |- ( S ^s ( B ^m I ) ) = ( S ^s ( ( Base ` S ) ^m I ) )
72	68, 71	eqtri 2428	. . . . . . . 8 |- T = ( S ^s ( ( Base ` S ) ^m I ) )
73	67, 72	oveq12i 6056	. . . . . . 7 |- ( W RingHom T ) = ( ( I mPoly ( S ↾s R ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) )
74	73	a1i 11	. . . . . 6 |- ( T. -> ( W RingHom T ) = ( ( I mPoly ( S ↾s R ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) )
75		evlsval.a	. . . . . . . . . . 11 |- A = (algSc ` W )
76	67	fveq2i 5694	. . . . . . . . . . 11 |- (algSc ` W ) = (algSc ` ( I mPoly ( S ↾s R ) ) )
77	75, 76	eqtri 2428	. . . . . . . . . 10 |- A = (algSc ` ( I mPoly ( S ↾s R ) ) )
78	77	coeq2i 4996	. . . . . . . . 9 |- ( f o. A ) = ( f o. (algSc ` ( I mPoly ( S ↾s R ) ) ) )
79		evlsval.x	. . . . . . . . . 10 |- X = ( x e. R |-> ( ( B ^m I ) X. { x } ) )
80	70	xpeq1i 4861	. . . . . . . . . . 11 |- ( ( B ^m I ) X. { x } ) = ( ( ( Base ` S ) ^m I ) X. { x } )
81	80	mpteq2i 4256	. . . . . . . . . 10 |- ( x e. R |-> ( ( B ^m I ) X. { x } ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) )
82	79, 81	eqtri 2428	. . . . . . . . 9 |- X = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) )
83	78, 82	eqeq12i 2421	. . . . . . . 8 |- ( ( f o. A ) = X <-> ( f o. (algSc ` ( I mPoly ( S ↾s R ) ) ) ) = ( x e. R |-> ( ( ( Base ` S ) ^m I ) X. { x } ) ) )
84		evlsval.v	. . . . . . . . . . 11 |- V = ( I mVar U )
85	65	oveq2i 6055	. . . . . . . . . . 11 |- ( I mVar U ) = ( I mVar ( S ↾s R ) )
86	84, 85	eqtri 2428	. . . . . . . . . 10 |- V = ( I mVar ( S ↾s R ) )
87	86	coeq2i 4996	. . . . . . . . 9 |- ( f o. V ) = ( f o. ( I mVar ( S ↾s R ) ) )
88		evlsval.y	. . . . . . . . . 10 |- Y = ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) )
89		eqid 2408	. . . . . . . . . . . 12 |- ( g ` x ) = ( g ` x )
90	70, 89	mpteq12i 4257	. . . . . . . . . . 11 |- ( g e. ( B ^m I ) |-> ( g ` x ) ) = ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) )
91	90	mpteq2i 4256	. . . . . . . . . 10 |- ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) )
92	88, 91	eqtri 2428	. . . . . . . . 9 |- Y = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) )
93	87, 92	eqeq12i 2421	. . . . . . . 8 |- ( ( f o. V ) = Y <-> ( f o. ( I mVar ( S ↾s R ) ) ) = ( x e. I |-> ( g e. ( ( Base ` S ) ^m I ) |-> ( g ` x ) ) ) )
94	83, 93	anbi12i 679	. . . . . . 7 |- ( ( ( 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 ) ) ) ) )
95	94	a1i 11	. . . . . 6 |- ( 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 ) ) ) ) ) )
96	74, 95	riotaeqbidv 6515	. . . . 5 |- ( 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 ) ) ) ) ) )
97	96	trud 1329	. . . 4 |- ( 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	63, 97	syl6eqr 2458	. . 3 |- ( 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 ) ) )
99	98	3ad2ant3 980	. 2 |- ( ( I e. _V /\ 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 ) ) )
100	48, 99	eqtrd 2440	1 |- ( ( I e. _V /\ S e. CRing /\ R e. (SubRing ` S ) ) -> Q = ( iota_ f e. ( W RingHom T ) ( ( f o. A ) = X /\ ( f o. V ) = Y ) ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   T. wtru 1322   = wceq 1649   e. wcel 1721   _Vcvv 2920   [_csb 3215   {csn 3778   e. cmpt 4230   X. cxp 4839   o. ccom 4845   ` cfv 5417  (class class class)co 6044   iota_crio 6505   ^m cmap 6981   Basecbs 13428   ↾_s cress 13429   ^_s cpws 13629   CRingccrg 15620   RingHom crh 15776  SubRingcsubrg 15823  algSccascl 16330   mVar cmvr 16366   mPoly cmpl 16367   evalSub ces 16368

This theorem is referenced by:  evlsval2  19898

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-rep 4284  ax-sep 4294  ax-nul 4302  ax-pr 4367

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-reu 2677  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-iun 4059  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-ov 6047  df-oprab 6048  df-mpt2 6049  df-riota 6512  df-evls 16379