Theorem mpfrcl 19518

Description: Reverse closure for the set of polynomial functions. (Contributed by Stefan O'Rear, 19-Mar-2015.)

Hypothesis

Ref	Expression
mpfrcl.q	|- Q = ran ( ( I evalSub S ) ` R )

Assertion

Ref	Expression
mpfrcl	|- ( X e. Q -> ( I e. _V /\ S e. CRing /\ R e. (SubRing ` S ) ) )

Proof of Theorem mpfrcl

Dummy variables a b f g i r s w x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ne0i 3921	. . 3 |- ( X e. ran ( ( I evalSub S ) ` R ) -> ran ( ( I evalSub S ) ` R ) =/= (/) )
2		mpfrcl.q	. . 3 |- Q = ran ( ( I evalSub S ) ` R )
3	1, 2	eleq2s 2719	. 2 |- ( X e. Q -> ran ( ( I evalSub S ) ` R ) =/= (/) )
4		rneq 5351	. . . 4 |- ( ( ( I evalSub S ) ` R ) = (/) -> ran ( ( I evalSub S ) ` R ) = ran (/) )
5		rn0 5377	. . . 4 |- ran (/) = (/)
6	4, 5	syl6eq 2672	. . 3 |- ( ( ( I evalSub S ) ` R ) = (/) -> ran ( ( I evalSub S ) ` R ) = (/) )
7	6	necon3i 2826	. 2 |- ( ran ( ( I evalSub S ) ` R ) =/= (/) -> ( ( I evalSub S ) ` R ) =/= (/) )
8		fveq1 6190	. . . . . . 7 |- ( ( I evalSub S ) = (/) -> ( ( I evalSub S ) ` R ) = ( (/) ` R ) )
9		0fv 6227	. . . . . . 7 |- ( (/) ` R ) = (/)
10	8, 9	syl6eq 2672	. . . . . 6 |- ( ( I evalSub S ) = (/) -> ( ( I evalSub S ) ` R ) = (/) )
11	10	necon3i 2826	. . . . 5 |- ( ( ( I evalSub S ) ` R ) =/= (/) -> ( I evalSub S ) =/= (/) )
12		reldmevls 19517	. . . . . . . 8 |- Rel dom evalSub
13	12	ovprc1 6684	. . . . . . 7 |- ( -. I e. _V -> ( I evalSub S ) = (/) )
14	13	necon1ai 2821	. . . . . 6 |- ( ( I evalSub S ) =/= (/) -> I e. _V )
15		n0 3931	. . . . . . 7 |- ( ( I evalSub S ) =/= (/) <-> E. a a e. ( I evalSub S ) )
16		df-evls 19506	. . . . . . . . . 10 |- 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 ) ) ) ) ) ) )
17	16	elmpt2cl2 6878	. . . . . . . . 9 |- ( a e. ( I evalSub S ) -> S e. CRing )
18	17	a1d 25	. . . . . . . 8 |- ( a e. ( I evalSub S ) -> ( I e. _V -> S e. CRing ) )
19	18	exlimiv 1858	. . . . . . 7 |- ( E. a a e. ( I evalSub S ) -> ( I e. _V -> S e. CRing ) )
20	15, 19	sylbi 207	. . . . . 6 |- ( ( I evalSub S ) =/= (/) -> ( I e. _V -> S e. CRing ) )
21	14, 20	jcai 559	. . . . 5 |- ( ( I evalSub S ) =/= (/) -> ( I e. _V /\ S e. CRing ) )
22	11, 21	syl 17	. . . 4 |- ( ( ( I evalSub S ) ` R ) =/= (/) -> ( I e. _V /\ S e. CRing ) )
23		fvex 6201	. . . . . . . . . . . . 13 |- ( Base ` s ) e. _V
24		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ b (SubRing ` s )
25		nfcsb1v 3549	. . . . . . . . . . . . . 14 |- F/_ b [_ ( Base ` s ) / b ]_ [_ ( 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 ) ) ) ) )
26	24, 25	nfmpt 4746	. . . . . . . . . . . . 13 |- F/_ b ( r e. (SubRing ` s ) |-> [_ ( Base ` s ) / b ]_ [_ ( 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 ) ) ) ) ) )
27		csbeq1a 3542	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) ) ) = [_ ( Base ` s ) / b ]_ [_ ( 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 ) ) ) ) ) )
28	27	mpteq2dv 4745	. . . . . . . . . . . . 13 |- ( 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 ) |-> [_ ( Base ` s ) / b ]_ [_ ( 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 ) ) ) ) ) ) )
29	23, 26, 28	csbief 3558	. . . . . . . . . . . 12 |- [_ ( 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 ) |-> [_ ( Base ` s ) / b ]_ [_ ( 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 ) ) ) ) ) )
30		fveq2 6191	. . . . . . . . . . . . . 14 |- ( s = S -> (SubRing ` s ) = (SubRing ` S ) )
31	30	adantl 482	. . . . . . . . . . . . 13 |- ( ( i = I /\ s = S ) -> (SubRing ` s ) = (SubRing ` S ) )
32		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( s = S -> ( Base ` s ) = ( Base ` S ) )
33	32	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( i = I /\ s = S ) -> ( Base ` s ) = ( Base ` S ) )
34	33	csbeq1d 3540	. . . . . . . . . . . . . 14 |- ( ( i = I /\ s = S ) -> [_ ( Base ` s ) / b ]_ [_ ( 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 ]_ [_ ( 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 ) ) ) ) ) )
35		id 22	. . . . . . . . . . . . . . . . . 18 |- ( i = I -> i = I )
36		oveq1 6657	. . . . . . . . . . . . . . . . . 18 |- ( s = S -> ( s ↾s r ) = ( S ↾s r ) )
37	35, 36	oveqan12d 6669	. . . . . . . . . . . . . . . . 17 |- ( ( i = I /\ s = S ) -> ( i mPoly ( s ↾s r ) ) = ( I mPoly ( S ↾s r ) ) )
38	37	csbeq1d 3540	. . . . . . . . . . . . . . . 16 |- ( ( i = I /\ s = 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 ) ) ) ) ) )
39		id 22	. . . . . . . . . . . . . . . . . . . 20 |- ( s = S -> s = S )
40		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20 |- ( i = I -> ( b ^m i ) = ( b ^m I ) )
41	39, 40	oveqan12rd 6670	. . . . . . . . . . . . . . . . . . 19 |- ( ( i = I /\ s = S ) -> ( s ^s ( b ^m i ) ) = ( S ^s ( b ^m I ) ) )
42	41	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ( i = I /\ s = S ) -> ( w RingHom ( s ^s ( b ^m i ) ) ) = ( w RingHom ( S ^s ( b ^m I ) ) ) )
43	40	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i = I /\ s = S ) -> ( b ^m i ) = ( b ^m I ) )
44	43	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i = I /\ s = S ) -> ( ( b ^m i ) X. { x } ) = ( ( b ^m I ) X. { x } ) )
45	44	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i = I /\ s = S ) -> ( x e. r |-> ( ( b ^m i ) X. { x } ) ) = ( x e. r |-> ( ( b ^m I ) X. { x } ) ) )
46	45	eqeq2d 2632	. . . . . . . . . . . . . . . . . . 19 |- ( ( i = I /\ s = S ) -> ( ( f o. (algSc ` w ) ) = ( x e. r |-> ( ( b ^m i ) X. { x } ) ) <-> ( f o. (algSc ` w ) ) = ( x e. r |-> ( ( b ^m I ) X. { x } ) ) ) )
47	35, 36	oveqan12d 6669	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i = I /\ s = S ) -> ( i mVar ( s ↾s r ) ) = ( I mVar ( S ↾s r ) ) )
48	47	coeq2d 5284	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i = I /\ s = S ) -> ( f o. ( i mVar ( s ↾s r ) ) ) = ( f o. ( I mVar ( S ↾s r ) ) ) )
49		simpl 473	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i = I /\ s = S ) -> i = I )
50	43	mpteq1d 4738	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i = I /\ s = S ) -> ( g e. ( b ^m i ) |-> ( g ` x ) ) = ( g e. ( b ^m I ) |-> ( g ` x ) ) )
51	49, 50	mpteq12dv 4733	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i = I /\ s = S ) -> ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) ) = ( x e. I |-> ( g e. ( b ^m I ) |-> ( g ` x ) ) ) )
52	48, 51	eqeq12d 2637	. . . . . . . . . . . . . . . . . . 19 |- ( ( i = I /\ s = S ) -> ( ( 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. ( b ^m I ) |-> ( g ` x ) ) ) ) )
53	46, 52	anbi12d 747	. . . . . . . . . . . . . . . . . 18 |- ( ( i = I /\ s = S ) -> ( ( ( 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 ` 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	42, 53	riotaeqbidv 6614	. . . . . . . . . . . . . . . . 17 |- ( ( i = I /\ s = S ) -> ( 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. ( 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 ) ) ) ) ) )
55	54	csbeq2dv 3992	. . . . . . . . . . . . . . . 16 |- ( ( i = I /\ s = 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 ) ) ) ) ) )
56	38, 55	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ( i = I /\ s = 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 ) ) ) ) ) )
57	56	csbeq2dv 3992	. . . . . . . . . . . . . 14 |- ( ( i = I /\ s = S ) -> [_ ( Base ` S ) / b ]_ [_ ( 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 ]_ [_ ( 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 ) ) ) ) ) )
58	34, 57	eqtrd 2656	. . . . . . . . . . . . 13 |- ( ( i = I /\ s = S ) -> [_ ( Base ` s ) / b ]_ [_ ( 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 ]_ [_ ( 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 ) ) ) ) ) )
59	31, 58	mpteq12dv 4733	. . . . . . . . . . . 12 |- ( ( i = I /\ s = S ) -> ( r e. (SubRing ` s ) |-> [_ ( Base ` s ) / b ]_ [_ ( 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 ) |-> [_ ( Base ` S ) / b ]_ [_ ( 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 ) ) ) ) ) ) )
60	29, 59	syl5eq 2668	. . . . . . . . . . 11 |- ( ( 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 ) |-> [_ ( Base ` S ) / b ]_ [_ ( 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 ) ) ) ) ) ) )
61		fvex 6201	. . . . . . . . . . . 12 |- (SubRing ` S ) e. _V
62	61	mptex 6486	. . . . . . . . . . 11 |- ( r e. (SubRing ` S ) |-> [_ ( Base ` S ) / b ]_ [_ ( 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 ) ) ) ) ) ) e. _V
63	60, 16, 62	ovmpt2a 6791	. . . . . . . . . 10 |- ( ( I e. _V /\ S e. CRing ) -> ( I evalSub S ) = ( r e. (SubRing ` S ) |-> [_ ( Base ` S ) / b ]_ [_ ( 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 ) ) ) ) ) ) )
64	63	dmeqd 5326	. . . . . . . . 9 |- ( ( I e. _V /\ S e. CRing ) -> dom ( I evalSub S ) = dom ( r e. (SubRing ` S ) |-> [_ ( Base ` S ) / b ]_ [_ ( 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 ) ) ) ) ) ) )
65		eqid 2622	. . . . . . . . . 10 |- ( r e. (SubRing ` S ) |-> [_ ( Base ` S ) / b ]_ [_ ( 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 ) |-> [_ ( Base ` S ) / b ]_ [_ ( 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 ) ) ) ) ) )
66	65	dmmptss 5631	. . . . . . . . 9 |- dom ( r e. (SubRing ` S ) |-> [_ ( Base ` S ) / b ]_ [_ ( 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 ) ) ) ) ) ) C_ (SubRing ` S )
67	64, 66	syl6eqss 3655	. . . . . . . 8 |- ( ( I e. _V /\ S e. CRing ) -> dom ( I evalSub S ) C_ (SubRing ` S ) )
68	67	ssneld 3605	. . . . . . 7 |- ( ( I e. _V /\ S e. CRing ) -> ( -. R e. (SubRing ` S ) -> -. R e. dom ( I evalSub S ) ) )
69		ndmfv 6218	. . . . . . 7 |- ( -. R e. dom ( I evalSub S ) -> ( ( I evalSub S ) ` R ) = (/) )
70	68, 69	syl6 35	. . . . . 6 |- ( ( I e. _V /\ S e. CRing ) -> ( -. R e. (SubRing ` S ) -> ( ( I evalSub S ) ` R ) = (/) ) )
71	70	necon1ad 2811	. . . . 5 |- ( ( I e. _V /\ S e. CRing ) -> ( ( ( I evalSub S ) ` R ) =/= (/) -> R e. (SubRing ` S ) ) )
72	71	com12 32	. . . 4 |- ( ( ( I evalSub S ) ` R ) =/= (/) -> ( ( I e. _V /\ S e. CRing ) -> R e. (SubRing ` S ) ) )
73	22, 72	jcai 559	. . 3 |- ( ( ( I evalSub S ) ` R ) =/= (/) -> ( ( I e. _V /\ S e. CRing ) /\ R e. (SubRing ` S ) ) )
74		df-3an 1039	. . 3 |- ( ( I e. _V /\ S e. CRing /\ R e. (SubRing ` S ) ) <-> ( ( I e. _V /\ S e. CRing ) /\ R e. (SubRing ` S ) ) )
75	73, 74	sylibr 224	. 2 |- ( ( ( I evalSub S ) ` R ) =/= (/) -> ( I e. _V /\ S e. CRing /\ R e. (SubRing ` S ) ) )
76	3, 7, 75	3syl 18	1 |- ( X e. Q -> ( I e. _V /\ S e. CRing /\ R e. (SubRing ` S ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   _Vcvv 3200   [_csb 3533   (/)c0 3915   {csn 4177   |-> cmpt 4729   X. cxp 5112   dom cdm 5114   ran crn 5115   o. ccom 5118   ` cfv 5888   iota_crio 6610  (class class class)co 6650   ^m cmap 7857   Basecbs 15857   ↾_s cress 15858   ^_s cpws 16107   CRingccrg 18548   RingHom crh 18712  SubRingcsubrg 18776  algSccascl 19311   mVar cmvr 19352   mPoly cmpl 19353   evalSub ces 19504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-evls 19506

This theorem is referenced by:  mpff  19533  mpfaddcl  19534  mpfmulcl  19535  mpfind  19536  pf1rcl  19713  mpfpf1  19715