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 mplring 
 |-  ( ( I e. _V /\ ( S |`s R ) e. Ring ) -> ( I mPoly ( S |`s R ) ) e. Ring )
47 39 45 46 syl2anc 
 |-  ( ph -> ( I mPoly ( S |`s R ) ) e. Ring )
48 47 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 )
49 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 } ) )
50 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 } ) ) )
51 29 50 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 } ) ) )
52 51 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 } ) ) )
53 49 52 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 } ) )
54 53 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 ) ) ) )
55 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 } ) )
56 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 } ) ) )
57 29 56 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 } ) ) )
58 57 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 } ) ) )
59 55 58 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 } ) )
60 59 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 ) ) ) )
61 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 ) ) ) )
62 48 54 60 61 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 ) ) ) )
63 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 ) ) ) )
64 19 24 63 3syl 
 |-  ( ph -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) GrpHom ( S ^s ( B ^m I ) ) ) )
65 64 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 ) ) ) )
66 eqid 
 |-  ( +g ` ( S ^s ( B ^m I ) ) ) = ( +g ` ( S ^s ( B ^m I ) ) )
67 25 36 66 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 ) ) )
68 65 54 60 67 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 ) ) )
69 40 adantr 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> S e. CRing )
70 ovexd 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( B ^m I ) e. _V )
71 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 ) ) ) )
72 71 54 ffvelrnd 
 |-  ( ( 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 ) ) ) )
73 71 60 ffvelrnd 
 |-  ( ( 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 ) ) ) )
74 23 26 69 70 72 73 2 66 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 ) ) )
75 68 74 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 ) ) )
76 simpl 
 |-  ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ph )
77 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 ) )
78 29 54 77 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 ) )
79 78 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 )
80 fvimacnvi 
 |-  ( ( Fun ( ( I evalSub S ) ` R ) /\ i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) -> ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } )
81 33 49 80 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 } )
82 79 81 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 } ) )
83 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 ) )
84 29 60 83 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 ) )
85 84 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 )
86 fvimacnvi 
 |-  ( ( Fun ( ( I evalSub S ) ` R ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) -> ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } )
87 33 55 86 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 } )
88 85 87 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 } ) )
89 fvex 
 |-  ( ( ( I evalSub S ) ` R ) ` i ) e. _V
90 fvex 
 |-  ( ( ( I evalSub S ) ` R ) ` j ) e. _V
91 eleq1 
 |-  ( f = ( ( ( I evalSub S ) ` R ) ` i ) -> ( f e. Q <-> ( ( ( I evalSub S ) ` R ) ` i ) e. Q ) )
92 vex 
 |-  f e. _V
93 92 9 elab 
 |-  ( f e. { x | ps } <-> ta )
94 eleq1 
 |-  ( f = ( ( ( I evalSub S ) ` R ) ` i ) -> ( f e. { x | ps } <-> ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) )
95 93 94 syl5bbr 
 |-  ( f = ( ( ( I evalSub S ) ` R ) ` i ) -> ( ta <-> ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) )
96 91 95 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 } ) ) )
97 eleq1 
 |-  ( g = ( ( ( I evalSub S ) ` R ) ` j ) -> ( g e. Q <-> ( ( ( I evalSub S ) ` R ) ` j ) e. Q ) )
98 vex 
 |-  g e. _V
99 98 10 elab 
 |-  ( g e. { x | ps } <-> et )
100 eleq1 
 |-  ( g = ( ( ( I evalSub S ) ` R ) ` j ) -> ( g e. { x | ps } <-> ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) )
101 99 100 syl5bbr 
 |-  ( g = ( ( ( I evalSub S ) ` R ) ` j ) -> ( et <-> ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) )
102 97 101 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 } ) ) )
103 96 102 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 } ) ) ) )
104 103 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 } ) ) ) ) )
105 ovex 
 |-  ( f oF .+ g ) e. _V
106 105 11 elab 
 |-  ( ( f oF .+ g ) e. { x | ps } <-> ze )
107 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 ) ) )
108 107 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 } ) )
109 106 108 syl5bbr 
 |-  ( ( 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 } ) )
110 104 109 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 } ) ) )
111 89 90 110 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 } )
112 76 82 88 111 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 } )
113 75 112 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 } )
114 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 } ) ) )
115 29 114 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 } ) ) )
116 115 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 } ) ) )
117 62 113 116 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 } ) )
118 117 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 } ) )
119 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 ) ) ) )
120 48 54 60 119 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 ) ) ) )
121 eqid 
 |-  ( mulGrp ` ( I mPoly ( S |`s R ) ) ) = ( mulGrp ` ( I mPoly ( S |`s R ) ) )
122 eqid 
 |-  ( mulGrp ` ( S ^s ( B ^m I ) ) ) = ( mulGrp ` ( S ^s ( B ^m I ) ) )
123 121 122 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 ) ) ) ) )
124 19 24 123 3syl 
 |-  ( ph -> ( ( I evalSub S ) ` R ) e. ( ( mulGrp ` ( I mPoly ( S |`s R ) ) ) MndHom ( mulGrp ` ( S ^s ( B ^m I ) ) ) ) )
125 124 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 ) ) ) ) )
126 121 25 mgpbas 
 |-  ( Base ` ( I mPoly ( S |`s R ) ) ) = ( Base ` ( mulGrp ` ( I mPoly ( S |`s R ) ) ) )
127 121 37 mgpplusg 
 |-  ( .r ` ( I mPoly ( S |`s R ) ) ) = ( +g ` ( mulGrp ` ( I mPoly ( S |`s R ) ) ) )
128 eqid 
 |-  ( .r ` ( S ^s ( B ^m I ) ) ) = ( .r ` ( S ^s ( B ^m I ) ) )
129 122 128 mgpplusg 
 |-  ( .r ` ( S ^s ( B ^m I ) ) ) = ( +g ` ( mulGrp ` ( S ^s ( B ^m I ) ) ) )
130 126 127 129 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 ) ) )
131 125 54 60 130 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 ) ) )
132 23 26 69 70 72 73 3 128 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 ) ) )
133 131 132 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 ) ) )
134 ovex 
 |-  ( f oF .x. g ) e. _V
135 134 12 elab 
 |-  ( ( f oF .x. g ) e. { x | ps } <-> si )
136 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 ) ) )
137 136 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 } ) )
138 135 137 syl5bbr 
 |-  ( ( 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 } ) )
139 104 138 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 } ) ) )
140 89 90 139 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 } )
141 76 82 88 140 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 } )
142 133 141 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 } )
143 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 } ) ) )
144 29 143 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 } ) ) )
145 144 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 } ) ) )
146 120 142 145 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 } ) )
147 146 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 } ) )
148 21 mplassa 
 |-  ( ( I e. _V /\ ( S |`s R ) e. CRing ) -> ( I mPoly ( S |`s R ) ) e. AssAlg )
149 39 43 148 syl2anc 
 |-  ( ph -> ( I mPoly ( S |`s R ) ) e. AssAlg )
150 eqid 
 |-  ( Scalar ` ( I mPoly ( S |`s R ) ) ) = ( Scalar ` ( I mPoly ( S |`s R ) ) )
151 38 150 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 ) ) ) )
152 eqid 
 |-  ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) = ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) )
153 152 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 ) ) ) )
154 149 151 153 3syl 
 |-  ( ph -> ( algSc ` ( I mPoly ( S |`s R ) ) ) : ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) --> ( Base ` ( I mPoly ( S |`s R ) ) ) )
155 154 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 ) ) ) )
156 21 39 43 mplsca 
 |-  ( ph -> ( S |`s R ) = ( Scalar ` ( I mPoly ( S |`s R ) ) ) )
157 156 fveq2d 
 |-  ( ph -> ( Base ` ( S |`s R ) ) = ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) )
158 157 eleq2d 
 |-  ( ph -> ( i e. ( Base ` ( S |`s R ) ) <-> i e. ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) ) )
159 158 biimpa 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> i e. ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) )
160 155 159 ffvelrnd 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
161 39 adantr 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> I e. _V )
162 40 adantr 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> S e. CRing )
163 41 adantr 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> R e. ( SubRing ` S ) )
164 1 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ B )
165 22 1 ressbas2 
 |-  ( R C_ B -> R = ( Base ` ( S |`s R ) ) )
166 41 164 165 3syl 
 |-  ( ph -> R = ( Base ` ( S |`s R ) ) )
167 166 eleq2d 
 |-  ( ph -> ( i e. R <-> i e. ( Base ` ( S |`s R ) ) ) )
168 167 biimpar 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> i e. R )
169 20 21 22 1 38 161 162 163 168 evlssca 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) ) = ( ( B ^m I ) X. { i } ) )
170 14 ralrimiva 
 |-  ( ph -> A. f e. R ch )
171 ovex 
 |-  ( B ^m I ) e. _V
172 snex 
 |-  { f } e. _V
173 171 172 xpex 
 |-  ( ( B ^m I ) X. { f } ) e. _V
174 173 7 elab 
 |-  ( ( ( B ^m I ) X. { f } ) e. { x | ps } <-> ch )
175 sneq 
 |-  ( f = i -> { f } = { i } )
176 175 xpeq2d 
 |-  ( f = i -> ( ( B ^m I ) X. { f } ) = ( ( B ^m I ) X. { i } ) )
177 176 eleq1d 
 |-  ( f = i -> ( ( ( B ^m I ) X. { f } ) e. { x | ps } <-> ( ( B ^m I ) X. { i } ) e. { x | ps } ) )
178 174 177 syl5bbr 
 |-  ( f = i -> ( ch <-> ( ( B ^m I ) X. { i } ) e. { x | ps } ) )
179 178 cbvralvw 
 |-  ( A. f e. R ch <-> A. i e. R ( ( B ^m I ) X. { i } ) e. { x | ps } )
180 170 179 sylib 
 |-  ( ph -> A. i e. R ( ( B ^m I ) X. { i } ) e. { x | ps } )
181 180 r19.21bi 
 |-  ( ( ph /\ i e. R ) -> ( ( B ^m I ) X. { i } ) e. { x | ps } )
182 168 181 syldan 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> ( ( B ^m I ) X. { i } ) e. { x | ps } )
183 169 182 eqeltrd 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) ) e. { x | ps } )
184 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 } ) ) )
185 29 184 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 } ) ) )
186 185 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 } ) ) )
187 160 183 186 mpbir2and 
 |-  ( ( ph /\ i e. ( Base ` ( S |`s R ) ) ) -> ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
188 187 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 } ) )
189 39 adantr 
 |-  ( ( ph /\ i e. I ) -> I e. _V )
190 45 adantr 
 |-  ( ( ph /\ i e. I ) -> ( S |`s R ) e. Ring )
191 simpr 
 |-  ( ( ph /\ i e. I ) -> i e. I )
192 21 35 25 189 190 191 mvrcl 
 |-  ( ( ph /\ i e. I ) -> ( ( I mVar ( S |`s R ) ) ` i ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
193 40 adantr 
 |-  ( ( ph /\ i e. I ) -> S e. CRing )
194 41 adantr 
 |-  ( ( ph /\ i e. I ) -> R e. ( SubRing ` S ) )
195 20 35 22 1 189 193 194 191 evlsvar 
 |-  ( ( ph /\ i e. I ) -> ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S |`s R ) ) ` i ) ) = ( g e. ( B ^m I ) |-> ( g ` i ) ) )
196 171 mptex 
 |-  ( g e. ( B ^m I ) |-> ( g ` f ) ) e. _V
197 196 8 elab 
 |-  ( ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } <-> th )
198 15 197 sylibr 
 |-  ( ( ph /\ f e. I ) -> ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } )
199 198 ralrimiva 
 |-  ( ph -> A. f e. I ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } )
200 fveq2 
 |-  ( f = i -> ( g ` f ) = ( g ` i ) )
201 200 mpteq2dv 
 |-  ( f = i -> ( g e. ( B ^m I ) |-> ( g ` f ) ) = ( g e. ( B ^m I ) |-> ( g ` i ) ) )
202 201 eleq1d 
 |-  ( f = i -> ( ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } <-> ( g e. ( B ^m I ) |-> ( g ` i ) ) e. { x | ps } ) )
203 202 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 } )
204 199 203 sylib 
 |-  ( ph -> A. i e. I ( g e. ( B ^m I ) |-> ( g ` i ) ) e. { x | ps } )
205 204 r19.21bi 
 |-  ( ( ph /\ i e. I ) -> ( g e. ( B ^m I ) |-> ( g ` i ) ) e. { x | ps } )
206 195 205 eqeltrd 
 |-  ( ( ph /\ i e. I ) -> ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S |`s R ) ) ` i ) ) e. { x | ps } )
207 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 } ) ) )
208 29 207 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 } ) ) )
209 208 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 } ) ) )
210 192 206 209 mpbir2and 
 |-  ( ( ph /\ i e. I ) -> ( ( I mVar ( S |`s R ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
211 210 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 } ) )
212 simpr 
 |-  ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> y e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
213 39 adantr 
 |-  ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> I e. _V )
214 43 adantr 
 |-  ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( S |`s R ) e. CRing )
215 34 35 21 36 37 38 25 118 147 188 211 212 213 214 mplind 
 |-  ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> y e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
216 fvimacnvi 
 |-  ( ( Fun ( ( I evalSub S ) ` R ) /\ y e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) -> ( ( ( I evalSub S ) ` R ) ` y ) e. { x | ps } )
217 33 215 216 syl2an2r 
 |-  ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` y ) e. { x | ps } )
218 eleq1 
 |-  ( ( ( ( I evalSub S ) ` R ) ` y ) = A -> ( ( ( ( I evalSub S ) ` R ) ` y ) e. { x | ps } <-> A e. { x | ps } ) )
219 217 218 syl5ibcom 
 |-  ( ( ph /\ y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` y ) = A -> A e. { x | ps } ) )
220 219 rexlimdva 
 |-  ( ph -> ( E. y e. ( Base ` ( I mPoly ( S |`s R ) ) ) ( ( ( I evalSub S ) ` R ) ` y ) = A -> A e. { x | ps } ) )
221 32 220 mpd 
 |-  ( ph -> A e. { x | ps } )
222 13 elabg 
 |-  ( A e. Q -> ( A e. { x | ps } <-> rh ) )
223 16 222 syl 
 |-  ( ph -> ( A e. { x | ps } <-> rh ) )
224 221 223 mpbid 
 |-  ( ph -> rh )