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 )