This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mpfind

Description: Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypotheses mpfind.cb 
|- B = ( Base ` S )
mpfind.cp 
|- .+ = ( +g ` S )
mpfind.ct 
|- .x. = ( .r ` S )
mpfind.cq 
|- Q = ran ( ( I evalSub S ) ` R )
mpfind.ad 
|- ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> ze )
mpfind.mu 
|- ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> si )
mpfind.wa 
|- ( x = ( ( B ^m I ) X. { f } ) -> ( ps <-> ch ) )
mpfind.wb 
|- ( x = ( g e. ( B ^m I ) |-> ( g ` f ) ) -> ( ps <-> th ) )
mpfind.wc 
|- ( x = f -> ( ps <-> ta ) )
mpfind.wd 
|- ( x = g -> ( ps <-> et ) )
mpfind.we 
|- ( x = ( f oF .+ g ) -> ( ps <-> ze ) )
mpfind.wf 
|- ( x = ( f oF .x. g ) -> ( ps <-> si ) )
mpfind.wg 
|- ( x = A -> ( ps <-> rh ) )
mpfind.co 
|- ( ( ph /\ f e. R ) -> ch )
mpfind.pr 
|- ( ( ph /\ f e. I ) -> th )
mpfind.a 
|- ( ph -> A e. Q )
Assertion mpfind 
|- ( ph -> rh )

Proof

Step Hyp Ref Expression
1 mpfind.cb 
 |-  B = ( Base ` S )
2 mpfind.cp 
 |-  .+ = ( +g ` S )
3 mpfind.ct 
 |-  .x. = ( .r ` S )
4 mpfind.cq 
 |-  Q = ran ( ( I evalSub S ) ` R )
5 mpfind.ad 
 |-  ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> ze )
6 mpfind.mu 
 |-  ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> si )
7 mpfind.wa 
 |-  ( x = ( ( B ^m I ) X. { f } ) -> ( ps <-> ch ) )
8 mpfind.wb 
 |-  ( x = ( g e. ( B ^m I ) |-> ( g ` f ) ) -> ( ps <-> th ) )
9 mpfind.wc 
 |-  ( x = f -> ( ps <-> ta ) )
10 mpfind.wd 
 |-  ( x = g -> ( ps <-> et ) )
11 mpfind.we 
 |-  ( x = ( f oF .+ g ) -> ( ps <-> ze ) )
12 mpfind.wf 
 |-  ( x = ( f oF .x. g ) -> ( ps <-> si ) )
13 mpfind.wg 
 |-  ( x = A -> ( ps <-> rh ) )
14 mpfind.co 
 |-  ( ( ph /\ f e. R ) -> ch )
15 mpfind.pr 
 |-  ( ( ph /\ f e. I ) -> th )
16 mpfind.a 
 |-  ( ph -> A e. Q )
17 16 4 eleqtrdi 
 |-  ( ph -> A e. ran ( ( I evalSub S ) ` R ) )
18 4 mpfrcl 
 |-  ( A e. Q -> ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) )
19 16 18 syl 
 |-  ( ph -> ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) )
20 eqid 
 |-  ( ( I evalSub S ) ` R ) = ( ( I evalSub S ) ` R )
21 eqid 
 |-  ( I mPoly ( S |`s R ) ) = ( I mPoly ( S |`s R ) )
22 eqid 
 |-  ( S |`s R ) = ( S |`s R )
23 eqid 
 |-  ( S ^s ( B ^m I ) ) = ( S ^s ( B ^m I ) )
24 20 21 22 23 1 evlsrhm 
 |-  ( ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( B ^m I ) ) ) )
25 eqid 
 |-  ( Base ` ( I mPoly ( S |`s R ) ) ) = ( Base ` ( I mPoly ( S |`s R ) ) )
26 eqid 
 |-  ( Base ` ( S ^s ( B ^m I ) ) ) = ( Base ` ( S ^s ( B ^m I ) ) )
27 25 26 rhmf 
 |-  ( ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( B ^m I ) ) ) -> ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S |`s R ) ) ) --> ( Base ` ( S ^s ( B ^m I ) ) ) )
28 19 24 27 3syl 
 |-  ( ph -> ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S |`s R ) ) ) --> ( Base ` ( S ^s ( B ^m I ) ) ) )
29 28 ffnd 
 |-  ( ph -> ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) )
30 fvelrnb 
 |-  ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) -> ( A e. ran ( ( I evalSub S ) ` R ) <-> E. y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ( ( ( I evalSub S ) ` R ) ` y ) = A ) )
31 29 30 syl 
 |-  ( ph -> ( A e. ran ( ( I evalSub S ) ` R ) <-> E. y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ( ( ( I evalSub S ) ` R ) ` y ) = A ) )
32 17 31 mpbid 
 |-  ( ph -> E. y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ( ( ( I evalSub S ) ` R ) ` y ) = A )
33 28 ffund 
 |-  ( ph -> Fun ( ( I evalSub S ) ` R ) )
34 eqid 
 |-  ( Base ` ( S |`s R ) ) = ( Base ` ( S |`s R ) )
35 eqid 
 |-  ( I mVar ( S |`s R ) ) = ( I mVar ( S |`s R ) )
36 eqid 
 |-  ( +g ` ( I mPoly ( S |`s R ) ) ) = ( +g ` ( I mPoly ( S |`s R ) ) )
37 eqid 
 |-  ( .r ` ( I mPoly ( S |`s R ) ) ) = ( .r ` ( I mPoly ( S |`s R ) ) )
38 eqid 
 |-  ( algSc ` ( I mPoly ( S |`s R ) ) ) = ( algSc ` ( I mPoly ( S |`s R ) ) )
39 19 simp1d 
 |-  ( ph -> I e. _V )
40 19 simp2d 
 |-  ( ph -> S e. CRing )
41 19 simp3d 
 |-  ( ph -> R e. ( SubRing ` S ) )
42 22 subrgcrng 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( S |`s R ) e. CRing )
43 40 41 42 syl2anc 
 |-  ( ph -> ( S |`s R ) e. CRing )
44 crngring 
 |-  ( ( S |`s R ) e. CRing -> ( S |`s R ) e. Ring )
45 43 44 syl 
 |-  ( ph -> ( S |`s R ) e. Ring )
46 21 39 45 mplringd 
 |-  ( ph -> ( I mPoly ( S |`s R ) ) e. Ring )
47 46 adantr 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( I mPoly ( S |`s R ) ) e. Ring )
48 simprl 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
49 elpreima 
 |-  ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) -> ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( i e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) ) )
50 29 49 syl 
 |-  ( ph -> ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( i e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) ) )
51 50 adantr 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( i e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) ) )
52 48 51 mpbid 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) )
53 52 simpld 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> i e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
54 simprr 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
55 elpreima 
 |-  ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) -> ( j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( j e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) )
56 29 55 syl 
 |-  ( ph -> ( j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( j e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) )
57 56 adantr 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( j e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) )
58 54 57 mpbid 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( j e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) )
59 58 simpld 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> j e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
60 25 36 ringacl 
 |-  ( ( ( I mPoly ( S |`s R ) ) e. Ring /\ i e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ j e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
61 47 53 59 60 syl3anc 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
62 rhmghm 
 |-  ( ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( B ^m I ) ) ) -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) GrpHom ( S ^s ( B ^m I ) ) ) )
63 19 24 62 3syl 
 |-  ( ph -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) GrpHom ( S ^s ( B ^m I ) ) ) )
64 63 adantr 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) GrpHom ( S ^s ( B ^m I ) ) ) )
65 eqid 
 |-  ( +g ` ( S ^s ( B ^m I ) ) ) = ( +g ` ( S ^s ( B ^m I ) ) )
66 25 36 65 ghmlin 
 |-  ( ( ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) GrpHom ( S ^s ( B ^m I ) ) ) /\ i e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ j e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) ( +g ` ( S ^s ( B ^m I ) ) ) ( ( ( I evalSub S ) ` R ) ` j ) ) )
67 64 53 59 66 syl3anc 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) ( +g ` ( S ^s ( B ^m I ) ) ) ( ( ( I evalSub S ) ` R ) ` j ) ) )
68 40 adantr 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> S e. CRing )
69 ovexd 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( B ^m I ) e. _V )
70 28 adantr 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S |`s R ) ) ) --> ( Base ` ( S ^s ( B ^m I ) ) ) )
71 70 53 ffvelcdmd 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` i ) e. ( Base ` ( S ^s ( B ^m I ) ) ) )
72 70 59 ffvelcdmd 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` j ) e. ( Base ` ( S ^s ( B ^m I ) ) ) )
73 23 26 68 69 71 72 2 65 pwsplusgval 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) ( +g ` ( S ^s ( B ^m I ) ) ) ( ( ( I evalSub S ) ` R ) ` j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) )
74 67 73 eqtrd 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) )
75 simpl 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ph )
76 fnfvelrn 
 |-  ( ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) /\ i e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` i ) e. ran ( ( I evalSub S ) ` R ) )
77 29 53 76 syl2an2r 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` i ) e. ran ( ( I evalSub S ) ` R ) )
78 77 4 eleqtrrdi 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` i ) e. Q )
79 fvimacnvi 
 |-  ( ( Fun ( ( I evalSub S ) ` R ) /\ i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) -> ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } )
80 33 48 79 syl2an2r 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } )
81 78 80 jca 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) )
82 fnfvelrn 
 |-  ( ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) /\ j e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` j ) e. ran ( ( I evalSub S ) ` R ) )
83 29 59 82 syl2an2r 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` j ) e. ran ( ( I evalSub S ) ` R ) )
84 83 4 eleqtrrdi 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` j ) e. Q )
85 fvimacnvi 
 |-  ( ( Fun ( ( I evalSub S ) ` R ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) -> ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } )
86 33 54 85 syl2an2r 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } )
87 84 86 jca 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) )
88 fvex 
 |-  ( ( ( I evalSub S ) ` R ) ` i ) e. _V
89 fvex 
 |-  ( ( ( I evalSub S ) ` R ) ` j ) e. _V
90 eleq1 
 |-  ( f = ( ( ( I evalSub S ) ` R ) ` i ) -> ( f e. Q <-> ( ( ( I evalSub S ) ` R ) ` i ) e. Q ) )
91 vex 
 |-  f e. _V
92 91 9 elab 
 |-  ( f e. { x | ps } <-> ta )
93 eleq1 
 |-  ( f = ( ( ( I evalSub S ) ` R ) ` i ) -> ( f e. { x | ps } <-> ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) )
94 92 93 bitr3id 
 |-  ( f = ( ( ( I evalSub S ) ` R ) ` i ) -> ( ta <-> ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) )
95 90 94 anbi12d 
 |-  ( f = ( ( ( I evalSub S ) ` R ) ` i ) -> ( ( f e. Q /\ ta ) <-> ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) ) )
96 eleq1 
 |-  ( g = ( ( ( I evalSub S ) ` R ) ` j ) -> ( g e. Q <-> ( ( ( I evalSub S ) ` R ) ` j ) e. Q ) )
97 vex 
 |-  g e. _V
98 97 10 elab 
 |-  ( g e. { x | ps } <-> et )
99 eleq1 
 |-  ( g = ( ( ( I evalSub S ) ` R ) ` j ) -> ( g e. { x | ps } <-> ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) )
100 98 99 bitr3id 
 |-  ( g = ( ( ( I evalSub S ) ` R ) ` j ) -> ( et <-> ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) )
101 96 100 anbi12d 
 |-  ( g = ( ( ( I evalSub S ) ` R ) ` j ) -> ( ( g e. Q /\ et ) <-> ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) )
102 95 101 bi2anan9 
 |-  ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) <-> ( ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) /\ ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) ) )
103 102 anbi2d 
 |-  ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) <-> ( ph /\ ( ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) /\ ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) ) ) )
104 ovex 
 |-  ( f oF .+ g ) e. _V
105 104 11 elab 
 |-  ( ( f oF .+ g ) e. { x | ps } <-> ze )
106 oveq12 
 |-  ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( f oF .+ g ) = ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) )
107 106 eleq1d 
 |-  ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ( f oF .+ g ) e. { x | ps } <-> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } ) )
108 105 107 bitr3id 
 |-  ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ze <-> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } ) )
109 103 108 imbi12d 
 |-  ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> ze ) <-> ( ( ph /\ ( ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) /\ ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } ) ) )
110 88 89 109 5 vtocl2 
 |-  ( ( ph /\ ( ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) /\ ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } )
111 75 81 87 110 syl12anc 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } )
112 74 111 eqeltrd 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) ) e. { x | ps } )
113 elpreima 
 |-  ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) -> ( ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) ) e. { x | ps } ) ) )
114 29 113 syl 
 |-  ( ph -> ( ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) ) e. { x | ps } ) ) )
115 114 adantr 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) ) e. { x | ps } ) ) )
116 61 112 115 mpbir2and 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
117 116 adantlr 
 |-  ( ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i ( +g ` ( I mPoly ( S |`s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
118 25 37 ringcl 
 |-  ( ( ( I mPoly ( S |`s R ) ) e. Ring /\ i e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ j e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
119 47 53 59 118 syl3anc 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
120 eqid 
 |-  ( mulGrp ` ( I mPoly ( S |`s R ) ) ) = ( mulGrp ` ( I mPoly ( S |`s R ) ) )
121 eqid 
 |-  ( mulGrp ` ( S ^s ( B ^m I ) ) ) = ( mulGrp ` ( S ^s ( B ^m I ) ) )
122 120 121 rhmmhm 
 |-  ( ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( B ^m I ) ) ) -> ( ( I evalSub S ) ` R ) e. ( ( mulGrp ` ( I mPoly ( S |`s R ) ) ) MndHom ( mulGrp ` ( S ^s ( B ^m I ) ) ) ) )
123 19 24 122 3syl 
 |-  ( ph -> ( ( I evalSub S ) ` R ) e. ( ( mulGrp ` ( I mPoly ( S |`s R ) ) ) MndHom ( mulGrp ` ( S ^s ( B ^m I ) ) ) ) )
124 123 adantr 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( I evalSub S ) ` R ) e. ( ( mulGrp ` ( I mPoly ( S |`s R ) ) ) MndHom ( mulGrp ` ( S ^s ( B ^m I ) ) ) ) )
125 120 25 mgpbas 
 |-  ( Base ` ( I mPoly ( S |`s R ) ) ) = ( Base ` ( mulGrp ` ( I mPoly ( S |`s R ) ) ) )
126 120 37 mgpplusg 
 |-  ( .r ` ( I mPoly ( S |`s R ) ) ) = ( +g ` ( mulGrp ` ( I mPoly ( S |`s R ) ) ) )
127 eqid 
 |-  ( .r ` ( S ^s ( B ^m I ) ) ) = ( .r ` ( S ^s ( B ^m I ) ) )
128 121 127 mgpplusg 
 |-  ( .r ` ( S ^s ( B ^m I ) ) ) = ( +g ` ( mulGrp ` ( S ^s ( B ^m I ) ) ) )
129 125 126 128 mhmlin 
 |-  ( ( ( ( I evalSub S ) ` R ) e. ( ( mulGrp ` ( I mPoly ( S |`s R ) ) ) MndHom ( mulGrp ` ( S ^s ( B ^m I ) ) ) ) /\ i e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ j e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) ( .r ` ( S ^s ( B ^m I ) ) ) ( ( ( I evalSub S ) ` R ) ` j ) ) )
130 124 53 59 129 syl3anc 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) ( .r ` ( S ^s ( B ^m I ) ) ) ( ( ( I evalSub S ) ` R ) ` j ) ) )
131 23 26 68 69 71 72 3 127 pwsmulrval 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) ( .r ` ( S ^s ( B ^m I ) ) ) ( ( ( I evalSub S ) ` R ) ` j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) )
132 130 131 eqtrd 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) )
133 ovex 
 |-  ( f oF .x. g ) e. _V
134 133 12 elab 
 |-  ( ( f oF .x. g ) e. { x | ps } <-> si )
135 oveq12 
 |-  ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( f oF .x. g ) = ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) )
136 135 eleq1d 
 |-  ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ( f oF .x. g ) e. { x | ps } <-> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } ) )
137 134 136 bitr3id 
 |-  ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( si <-> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } ) )
138 103 137 imbi12d 
 |-  ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> si ) <-> ( ( ph /\ ( ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) /\ ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } ) ) )
139 88 89 138 6 vtocl2 
 |-  ( ( ph /\ ( ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) /\ ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } )
140 75 81 87 139 syl12anc 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } )
141 132 140 eqeltrd 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) ) e. { x | ps } )
142 elpreima 
 |-  ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) -> ( ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) ) e. { x | ps } ) ) )
143 29 142 syl 
 |-  ( ph -> ( ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) ) e. { x | ps } ) ) )
144 143 adantr 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) ) e. { x | ps } ) ) )
145 119 141 144 mpbir2and 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
146 145 adantlr 
 |-  ( ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i ( .r ` ( I mPoly ( S |`s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
147 21 mplassa 
 |-  ( ( I e. _V /\ ( S |`s R ) e. CRing ) -> ( I mPoly ( S |`s R ) ) e. AssAlg )
148 39 43 147 syl2anc 
 |-  ( ph -> ( I mPoly ( S |`s R ) ) e. AssAlg )
149 eqid 
 |-  ( Scalar ` ( I mPoly ( S |`s R ) ) ) = ( Scalar ` ( I mPoly ( S |`s R ) ) )
150 38 149 asclrhm 
 |-  ( ( I mPoly ( S |`s R ) ) e. AssAlg -> ( algSc ` ( I mPoly ( S |`s R ) ) ) e. ( ( Scalar ` ( I mPoly ( S |`s R ) ) ) RingHom ( I mPoly ( S |`s R ) ) ) )
151 eqid 
 |-  ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) = ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) )
152 151 25 rhmf 
 |-  ( ( algSc ` ( I mPoly ( S |`s R ) ) ) e. ( ( Scalar ` ( I mPoly ( S |`s R ) ) ) RingHom ( I mPoly ( S |`s R ) ) ) -> ( algSc ` ( I mPoly ( S |`s R ) ) ) : ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) --> ( Base ` ( I mPoly ( S |`s R ) ) ) )
153 148 150 152 3syl 
 |-  ( ph -> ( algSc ` ( I mPoly ( S |`s R ) ) ) : ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) --> ( Base ` ( I mPoly ( S |`s R ) ) ) )
154 153 adantr 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> ( algSc ` ( I mPoly ( S |`s R ) ) ) : ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) --> ( Base ` ( I mPoly ( S |`s R ) ) ) )
155 21 39 43 mplsca 
 |-  ( ph -> ( S |`s R ) = ( Scalar ` ( I mPoly ( S |`s R ) ) ) )
156 155 fveq2d 
 |-  ( ph -> ( Base ` ( S |`s R ) ) = ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) )
157 156 eleq2d 
 |-  ( ph -> ( i e. ( Base ` ( S |`s R ) ) <-> i e. ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) ) )
158 157 biimpa 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> i e. ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) )
159 154 158 ffvelcdmd 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
160 39 adantr 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> I e. _V )
161 40 adantr 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> S e. CRing )
162 41 adantr 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> R e. ( SubRing ` S ) )
163 1 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ B )
164 22 1 ressbas2 
 |-  ( R C_ B -> R = ( Base ` ( S |`s R ) ) )
165 41 163 164 3syl 
 |-  ( ph -> R = ( Base ` ( S |`s R ) ) )
166 165 eleq2d 
 |-  ( ph -> ( i e. R <-> i e. ( Base ` ( S |`s R ) ) ) )
167 166 biimpar 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> i e. R )
168 20 21 22 1 38 160 161 162 167 evlssca 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) ) = ( ( B ^m I ) X. { i } ) )
169 14 ralrimiva 
 |-  ( ph -> A. f e. R ch )
170 ovex 
 |-  ( B ^m I ) e. _V
171 vsnex 
 |-  { f } e. _V
172 170 171 xpex 
 |-  ( ( B ^m I ) X. { f } ) e. _V
173 172 7 elab 
 |-  ( ( ( B ^m I ) X. { f } ) e. { x | ps } <-> ch )
174 sneq 
 |-  ( f = i -> { f } = { i } )
175 174 xpeq2d 
 |-  ( f = i -> ( ( B ^m I ) X. { f } ) = ( ( B ^m I ) X. { i } ) )
176 175 eleq1d 
 |-  ( f = i -> ( ( ( B ^m I ) X. { f } ) e. { x | ps } <-> ( ( B ^m I ) X. { i } ) e. { x | ps } ) )
177 173 176 bitr3id 
 |-  ( f = i -> ( ch <-> ( ( B ^m I ) X. { i } ) e. { x | ps } ) )
178 177 cbvralvw 
 |-  ( A. f e. R ch <-> A. i e. R ( ( B ^m I ) X. { i } ) e. { x | ps } )
179 169 178 sylib 
 |-  ( ph -> A. i e. R ( ( B ^m I ) X. { i } ) e. { x | ps } )
180 179 r19.21bi 
 |-  ( ( ph /\ i e. R ) -> ( ( B ^m I ) X. { i } ) e. { x | ps } )
181 167 180 syldan 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> ( ( B ^m I ) X. { i } ) e. { x | ps } )
182 168 181 eqeltrd 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) ) e. { x | ps } )
183 elpreima 
 |-  ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) -> ( ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) ) e. { x | ps } ) ) )
184 29 183 syl 
 |-  ( ph -> ( ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) ) e. { x | ps } ) ) )
185 184 adantr 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> ( ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) ) e. { x | ps } ) ) )
186 159 182 185 mpbir2and 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
187 186 adantlr 
 |-  ( ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) /\ i e. ( Base ` ( S |`s R ) ) ) -> ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
188 39 adantr 
 |-  ( ( ph /\ i e. I ) -> I e. _V )
189 45 adantr 
 |-  ( ( ph /\ i e. I ) -> ( S |`s R ) e. Ring )
190 simpr 
 |-  ( ( ph /\ i e. I ) -> i e. I )
191 21 35 25 188 189 190 mvrcl 
 |-  ( ( ph /\ i e. I ) -> ( ( I mVar ( S |`s R ) ) ` i ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
192 40 adantr 
 |-  ( ( ph /\ i e. I ) -> S e. CRing )
193 41 adantr 
 |-  ( ( ph /\ i e. I ) -> R e. ( SubRing ` S ) )
194 20 35 22 1 188 192 193 190 evlsvar 
 |-  ( ( ph /\ i e. I ) -> ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S |`s R ) ) ` i ) ) = ( g e. ( B ^m I ) |-> ( g ` i ) ) )
195 170 mptex 
 |-  ( g e. ( B ^m I ) |-> ( g ` f ) ) e. _V
196 195 8 elab 
 |-  ( ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } <-> th )
197 15 196 sylibr 
 |-  ( ( ph /\ f e. I ) -> ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } )
198 197 ralrimiva 
 |-  ( ph -> A. f e. I ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } )
199 fveq2 
 |-  ( f = i -> ( g ` f ) = ( g ` i ) )
200 199 mpteq2dv 
 |-  ( f = i -> ( g e. ( B ^m I ) |-> ( g ` f ) ) = ( g e. ( B ^m I ) |-> ( g ` i ) ) )
201 200 eleq1d 
 |-  ( f = i -> ( ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } <-> ( g e. ( B ^m I ) |-> ( g ` i ) ) e. { x | ps } ) )
202 201 cbvralvw 
 |-  ( A. f e. I ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } <-> A. i e. I ( g e. ( B ^m I ) |-> ( g ` i ) ) e. { x | ps } )
203 198 202 sylib 
 |-  ( ph -> A. i e. I ( g e. ( B ^m I ) |-> ( g ` i ) ) e. { x | ps } )
204 203 r19.21bi 
 |-  ( ( ph /\ i e. I ) -> ( g e. ( B ^m I ) |-> ( g ` i ) ) e. { x | ps } )
205 194 204 eqeltrd 
 |-  ( ( ph /\ i e. I ) -> ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S |`s R ) ) ` i ) ) e. { x | ps } )
206 elpreima 
 |-  ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) -> ( ( ( I mVar ( S |`s R ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( ( I mVar ( S |`s R ) ) ` i ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S |`s R ) ) ` i ) ) e. { x | ps } ) ) )
207 29 206 syl 
 |-  ( ph -> ( ( ( I mVar ( S |`s R ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( ( I mVar ( S |`s R ) ) ` i ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S |`s R ) ) ` i ) ) e. { x | ps } ) ) )
208 207 adantr 
 |-  ( ( ph /\ i e. I ) -> ( ( ( I mVar ( S |`s R ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( ( I mVar ( S |`s R ) ) ` i ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S |`s R ) ) ` i ) ) e. { x | ps } ) ) )
209 191 205 208 mpbir2and 
 |-  ( ( ph /\ i e. I ) -> ( ( I mVar ( S |`s R ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
210 209 adantlr 
 |-  ( ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) /\ i e. I ) -> ( ( I mVar ( S |`s R ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
211 simpr 
 |-  ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> y e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
212 39 adantr 
 |-  ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> I e. _V )
213 43 adantr 
 |-  ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( S |`s R ) e. CRing )
214 34 35 21 36 37 38 25 117 146 187 210 211 212 213 mplind 
 |-  ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> y e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
215 fvimacnvi 
 |-  ( ( Fun ( ( I evalSub S ) ` R ) /\ y e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) -> ( ( ( I evalSub S ) ` R ) ` y ) e. { x | ps } )
216 33 214 215 syl2an2r 
 |-  ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` y ) e. { x | ps } )
217 eleq1 
 |-  ( ( ( ( I evalSub S ) ` R ) ` y ) = A -> ( ( ( ( I evalSub S ) ` R ) ` y ) e. { x | ps } <-> A e. { x | ps } ) )
218 216 217 syl5ibcom 
 |-  ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` y ) = A -> A e. { x | ps } ) )
219 218 rexlimdva 
 |-  ( ph -> ( E. y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ( ( ( I evalSub S ) ` R ) ` y ) = A -> A e. { x | ps } ) )
220 32 219 mpd 
 |-  ( ph -> A e. { x | ps } )
221 13 elabg 
 |-  ( A e. Q -> ( A e. { x | ps } <-> rh ) )
222 16 221 syl 
 |-  ( ph -> ( A e. { x | ps } <-> rh ) )
223 220 222 mpbid 
 |-  ( ph -> rh )