Metamath Proof Explorer

Theorem mpfrcl

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

Ref Expression
Hypothesis mpfrcl.q 
|- Q = ran ( ( I evalSub S ) ` R )
Assertion mpfrcl 
|- ( X e. Q -> ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) )

Proof

Step Hyp Ref Expression
1 mpfrcl.q 
 |-  Q = ran ( ( I evalSub S ) ` R )
2 ne0i 
 |-  ( X e. ran ( ( I evalSub S ) ` R ) -> ran ( ( I evalSub S ) ` R ) =/= (/) )
3 2 1 eleq2s 
 |-  ( X e. Q -> ran ( ( I evalSub S ) ` R ) =/= (/) )
4 rneq 
 |-  ( ( ( I evalSub S ) ` R ) = (/) -> ran ( ( I evalSub S ) ` R ) = ran (/) )
5 rn0 
 |-  ran (/) = (/)
6 4 5 eqtrdi 
 |-  ( ( ( I evalSub S ) ` R ) = (/) -> ran ( ( I evalSub S ) ` R ) = (/) )
7 6 necon3i 
 |-  ( ran ( ( I evalSub S ) ` R ) =/= (/) -> ( ( I evalSub S ) ` R ) =/= (/) )
8 fveq1 
 |-  ( ( I evalSub S ) = (/) -> ( ( I evalSub S ) ` R ) = ( (/) ` R ) )
9 0fv 
 |-  ( (/) ` R ) = (/)
10 8 9 eqtrdi 
 |-  ( ( I evalSub S ) = (/) -> ( ( I evalSub S ) ` R ) = (/) )
11 10 necon3i 
 |-  ( ( ( I evalSub S ) ` R ) =/= (/) -> ( I evalSub S ) =/= (/) )
12 reldmevls 
 |-  Rel dom evalSub
13 12 ovprc1 
 |-  ( -. I e. _V -> ( I evalSub S ) = (/) )
14 13 necon1ai 
 |-  ( ( I evalSub S ) =/= (/) -> I e. _V )
15 n0 
 |-  ( ( I evalSub S ) =/= (/) <-> E. a a e. ( I evalSub S ) )
16 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 ) ) ) ) ) ) )
17 16 elmpocl2 
 |-  ( a e. ( I evalSub S ) -> S e. CRing )
18 17 a1d 
 |-  ( a e. ( I evalSub S ) -> ( I e. _V -> S e. CRing ) )
19 18 exlimiv 
 |-  ( E. a a e. ( I evalSub S ) -> ( I e. _V -> S e. CRing ) )
20 15 19 sylbi 
 |-  ( ( I evalSub S ) =/= (/) -> ( I e. _V -> S e. CRing ) )
21 14 20 jcai 
 |-  ( ( I evalSub S ) =/= (/) -> ( I e. _V /\ S e. CRing ) )
22 11 21 syl 
 |-  ( ( ( I evalSub S ) ` R ) =/= (/) -> ( I e. _V /\ S e. CRing ) )
23 fvex 
 |-  ( Base ` s ) e. _V
24 nfcv 
 |-  F/_ b ( SubRing ` s )
25 nfcsb1v 
 |-  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 
 |-  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 
 |-  ( 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 
 |-  ( 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 
 |-  [_ ( 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 
 |-  ( s = S -> ( SubRing ` s ) = ( SubRing ` S ) )
31 30 adantl 
 |-  ( ( i = I /\ s = S ) -> ( SubRing ` s ) = ( SubRing ` S ) )
32 fveq2 
 |-  ( s = S -> ( Base ` s ) = ( Base ` S ) )
33 32 adantl 
 |-  ( ( i = I /\ s = S ) -> ( Base ` s ) = ( Base ` S ) )
34 33 csbeq1d 
 |-  ( ( 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 
 |-  ( i = I -> i = I )
36 oveq1 
 |-  ( s = S -> ( s |`s r ) = ( S |`s r ) )
37 35 36 oveqan12d 
 |-  ( ( i = I /\ s = S ) -> ( i mPoly ( s |`s r ) ) = ( I mPoly ( S |`s r ) ) )
38 37 csbeq1d 
 |-  ( ( 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 
 |-  ( s = S -> s = S )
40 oveq2 
 |-  ( i = I -> ( b ^m i ) = ( b ^m I ) )
41 39 40 oveqan12rd 
 |-  ( ( i = I /\ s = S ) -> ( s ^s ( b ^m i ) ) = ( S ^s ( b ^m I ) ) )
42 41 oveq2d 
 |-  ( ( i = I /\ s = S ) -> ( w RingHom ( s ^s ( b ^m i ) ) ) = ( w RingHom ( S ^s ( b ^m I ) ) ) )
43 40 adantr 
 |-  ( ( i = I /\ s = S ) -> ( b ^m i ) = ( b ^m I ) )
44 43 xpeq1d 
 |-  ( ( i = I /\ s = S ) -> ( ( b ^m i ) X. { x } ) = ( ( b ^m I ) X. { x } ) )
45 44 mpteq2dv 
 |-  ( ( i = I /\ s = S ) -> ( x e. r |-> ( ( b ^m i ) X. { x } ) ) = ( x e. r |-> ( ( b ^m I ) X. { x } ) ) )
46 45 eqeq2d 
 |-  ( ( 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 
 |-  ( ( i = I /\ s = S ) -> ( i mVar ( s |`s r ) ) = ( I mVar ( S |`s r ) ) )
48 47 coeq2d 
 |-  ( ( i = I /\ s = S ) -> ( f o. ( i mVar ( s |`s r ) ) ) = ( f o. ( I mVar ( S |`s r ) ) ) )
49 simpl 
 |-  ( ( i = I /\ s = S ) -> i = I )
50 43 mpteq1d 
 |-  ( ( i = I /\ s = S ) -> ( g e. ( b ^m i ) |-> ( g ` x ) ) = ( g e. ( b ^m I ) |-> ( g ` x ) ) )
51 49 50 mpteq12dv 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( 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 eqtrid 
 |-  ( ( 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 
 |-  ( SubRing ` S ) e. _V
62 61 mptex 
 |-  ( 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 ovmpoa 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( 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 
 |-  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 eqsstrdi 
 |-  ( ( I e. _V /\ S e. CRing ) -> dom ( I evalSub S ) C_ ( SubRing ` S ) )
68 67 ssneld 
 |-  ( ( I e. _V /\ S e. CRing ) -> ( -. R e. ( SubRing ` S ) -> -. R e. dom ( I evalSub S ) ) )
69 ndmfv 
 |-  ( -. R e. dom ( I evalSub S ) -> ( ( I evalSub S ) ` R ) = (/) )
70 68 69 syl6 
 |-  ( ( I e. _V /\ S e. CRing ) -> ( -. R e. ( SubRing ` S ) -> ( ( I evalSub S ) ` R ) = (/) ) )
71 70 necon1ad 
 |-  ( ( I e. _V /\ S e. CRing ) -> ( ( ( I evalSub S ) ` R ) =/= (/) -> R e. ( SubRing ` S ) ) )
72 71 com12 
 |-  ( ( ( I evalSub S ) ` R ) =/= (/) -> ( ( I e. _V /\ S e. CRing ) -> R e. ( SubRing ` S ) ) )
73 22 72 jcai 
 |-  ( ( ( I evalSub S ) ` R ) =/= (/) -> ( ( I e. _V /\ S e. CRing ) /\ R e. ( SubRing ` S ) ) )
74 df-3an 
 |-  ( ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) <-> ( ( I e. _V /\ S e. CRing ) /\ R e. ( SubRing ` S ) ) )
75 73 74 sylibr 
 |-  ( ( ( I evalSub S ) ` R ) =/= (/) -> ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) )
76 3 7 75 3syl 
 |-  ( X e. Q -> ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) )