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 bitr3id
 |-  ( 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 bitr3id
 |-  ( 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 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 } ) )
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 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 } ) )
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 bitr3id
 |-  ( 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 )