MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpfind Unicode version

Theorem mpfind 19481
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.)
Hypotheses
Ref Expression
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  o F  .+  g )  ->  ( ps  <->  ze )
)
mpfind.wf  |-  ( x  =  ( f  o F  .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
Ref Expression
mpfind  |-  ( ph  ->  rh )
Distinct variable groups:    ch, x    et, x    ph, f, g    ps, f, g    rh, x    si, x    ta, x    th, x    ze, x    x, A    B, f, g, x   
f, I, g, x    .+ , f, g, x    Q, f, g    R, f, g    S, f, g    .x. , f,
g, x
Allowed substitution hints:    ph( x)    ps( x)    ch( f, g)    th( f,
g)    ta( f, g)    et( f, g)    ze( f, g)    si( f, g)    rh( f,
g)    A( f, g)    Q( x)    R( x)    S( x)

Proof of Theorem mpfind
Dummy variables  i 
j  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mpfind.a . . . . 5  |-  ( ph  ->  A  e.  Q )
2 mpfind.cq . . . . 5  |-  Q  =  ran  ( ( I evalSub  S ) `  R
)
31, 2syl6eleq 2406 . . . 4  |-  ( ph  ->  A  e.  ran  (
( I evalSub  S ) `  R ) )
42mpfrcl 19455 . . . . . . . . 9  |-  ( A  e.  Q  ->  (
I  e.  _V  /\  S  e.  CRing  /\  R  e.  (SubRing `  S )
) )
51, 4syl 15 . . . . . . . 8  |-  ( ph  ->  ( I  e.  _V  /\  S  e.  CRing  /\  R  e.  (SubRing `  S )
) )
6 eqid 2316 . . . . . . . . 9  |-  ( ( I evalSub  S ) `  R
)  =  ( ( I evalSub  S ) `  R
)
7 eqid 2316 . . . . . . . . 9  |-  ( I mPoly 
( Ss  R ) )  =  ( I mPoly  ( Ss  R ) )
8 eqid 2316 . . . . . . . . 9  |-  ( Ss  R )  =  ( Ss  R )
9 eqid 2316 . . . . . . . . 9  |-  ( S  ^s  ( B  ^m  I
) )  =  ( S  ^s  ( B  ^m  I
) )
10 mpfind.cb . . . . . . . . 9  |-  B  =  ( Base `  S
)
116, 7, 8, 9, 10evlsrhm 19458 . . . . . . . 8  |-  ( ( I  e.  _V  /\  S  e.  CRing  /\  R  e.  (SubRing `  S )
)  ->  ( (
I evalSub  S ) `  R
)  e.  ( ( I mPoly  ( Ss  R ) ) RingHom  ( S  ^s  ( B  ^m  I ) ) ) )
125, 11syl 15 . . . . . . 7  |-  ( ph  ->  ( ( I evalSub  S
) `  R )  e.  ( ( I mPoly  ( Ss  R ) ) RingHom  ( S  ^s  ( B  ^m  I
) ) ) )
13 eqid 2316 . . . . . . . 8  |-  ( Base `  ( I mPoly  ( Ss  R ) ) )  =  ( Base `  (
I mPoly  ( Ss  R ) ) )
14 eqid 2316 . . . . . . . 8  |-  ( Base `  ( S  ^s  ( B  ^m  I ) ) )  =  ( Base `  ( S  ^s  ( B  ^m  I ) ) )
1513, 14rhmf 15553 . . . . . . 7  |-  ( ( ( I evalSub  S ) `
 R )  e.  ( ( I mPoly  ( Ss  R ) ) RingHom  ( S  ^s  ( B  ^m  I
) ) )  -> 
( ( I evalSub  S
) `  R ) : ( Base `  (
I mPoly  ( Ss  R ) ) ) --> ( Base `  ( S  ^s  ( B  ^m  I ) ) ) )
1612, 15syl 15 . . . . . 6  |-  ( ph  ->  ( ( I evalSub  S
) `  R ) : ( Base `  (
I mPoly  ( Ss  R ) ) ) --> ( Base `  ( S  ^s  ( B  ^m  I ) ) ) )
17 ffn 5427 . . . . . 6  |-  ( ( ( I evalSub  S ) `
 R ) : ( Base `  (
I mPoly  ( Ss  R ) ) ) --> ( Base `  ( S  ^s  ( B  ^m  I ) ) )  ->  ( (
I evalSub  S ) `  R
)  Fn  ( Base `  ( I mPoly  ( Ss  R ) ) ) )
1816, 17syl 15 . . . . 5  |-  ( ph  ->  ( ( I evalSub  S
) `  R )  Fn  ( Base `  (
I mPoly  ( Ss  R ) ) ) )
19 fvelrnb 5608 . . . . 5  |-  ( ( ( I evalSub  S ) `
 R )  Fn  ( Base `  (
I mPoly  ( Ss  R ) ) )  ->  ( A  e.  ran  ( ( I evalSub  S ) `  R
)  <->  E. y  e.  (
Base `  ( I mPoly  ( Ss  R ) ) ) ( ( ( I evalSub  S ) `  R
) `  y )  =  A ) )
2018, 19syl 15 . . . 4  |-  ( ph  ->  ( A  e.  ran  ( ( I evalSub  S
) `  R )  <->  E. y  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) ( ( ( I evalSub  S
) `  R ) `  y )  =  A ) )
213, 20mpbid 201 . . 3  |-  ( ph  ->  E. y  e.  (
Base `  ( I mPoly  ( Ss  R ) ) ) ( ( ( I evalSub  S ) `  R
) `  y )  =  A )
22 ffun 5429 . . . . . . . 8  |-  ( ( ( I evalSub  S ) `
 R ) : ( Base `  (
I mPoly  ( Ss  R ) ) ) --> ( Base `  ( S  ^s  ( B  ^m  I ) ) )  ->  Fun  ( ( I evalSub  S ) `  R
) )
2316, 22syl 15 . . . . . . 7  |-  ( ph  ->  Fun  ( ( I evalSub  S ) `  R
) )
2423adantr 451 . . . . . 6  |-  ( (
ph  /\  y  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) )  ->  Fun  ( ( I evalSub  S ) `  R
) )
25 eqid 2316 . . . . . . 7  |-  ( Base `  ( Ss  R ) )  =  ( Base `  ( Ss  R ) )
26 eqid 2316 . . . . . . 7  |-  ( I mVar  ( Ss  R ) )  =  ( I mVar  ( Ss  R ) )
27 eqid 2316 . . . . . . 7  |-  ( +g  `  ( I mPoly  ( Ss  R ) ) )  =  ( +g  `  (
I mPoly  ( Ss  R ) ) )
28 eqid 2316 . . . . . . 7  |-  ( .r
`  ( I mPoly  ( Ss  R ) ) )  =  ( .r `  ( I mPoly  ( Ss  R
) ) )
29 eqid 2316 . . . . . . 7  |-  (algSc `  ( I mPoly  ( Ss  R
) ) )  =  (algSc `  ( I mPoly  ( Ss  R ) ) )
305simp1d 967 . . . . . . . . . . . 12  |-  ( ph  ->  I  e.  _V )
315simp2d 968 . . . . . . . . . . . . . 14  |-  ( ph  ->  S  e.  CRing )
325simp3d 969 . . . . . . . . . . . . . 14  |-  ( ph  ->  R  e.  (SubRing `  S
) )
338subrgcrng 15598 . . . . . . . . . . . . . 14  |-  ( ( S  e.  CRing  /\  R  e.  (SubRing `  S )
)  ->  ( Ss  R
)  e.  CRing )
3431, 32, 33syl2anc 642 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Ss  R )  e.  CRing )
35 crngrng 15400 . . . . . . . . . . . . 13  |-  ( ( Ss  R )  e.  CRing  -> 
( Ss  R )  e.  Ring )
3634, 35syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( Ss  R )  e.  Ring )
377mplrng 16245 . . . . . . . . . . . 12  |-  ( ( I  e.  _V  /\  ( Ss  R )  e.  Ring )  ->  ( I mPoly  ( Ss  R ) )  e. 
Ring )
3830, 36, 37syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( I mPoly  ( Ss  R ) )  e.  Ring )
3938adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( I mPoly  ( Ss  R ) )  e. 
Ring )
40 simprl 732 . . . . . . . . . . . 12  |-  ( (
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 } ) )
41 elpreima 5683 . . . . . . . . . . . . . 14  |-  ( ( ( I evalSub  S ) `
 R )  Fn  ( Base `  (
I mPoly  ( Ss  R ) ) )  ->  (
i  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } )  <->  ( i  e.  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  i )  e.  {
x  |  ps }
) ) )
4218, 41syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  <->  ( i  e.  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  i )  e.  {
x  |  ps }
) ) )
4342adantr 451 . . . . . . . . . . . 12  |-  ( (
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  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  i )  e.  {
x  |  ps }
) ) )
4440, 43mpbid 201 . . . . . . . . . . 11  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( i  e.  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  i )  e.  {
x  |  ps }
) )
4544simpld 445 . . . . . . . . . 10  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  i  e.  (
Base `  ( I mPoly  ( Ss  R ) ) ) )
46 simprr 733 . . . . . . . . . . . 12  |-  ( (
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 } ) )
47 elpreima 5683 . . . . . . . . . . . . . 14  |-  ( ( ( I evalSub  S ) `
 R )  Fn  ( Base `  (
I mPoly  ( Ss  R ) ) )  ->  (
j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } )  <->  ( j  e.  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  j )  e.  {
x  |  ps }
) ) )
4818, 47syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( j  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  <->  ( j  e.  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  j )  e.  {
x  |  ps }
) ) )
4948adantr 451 . . . . . . . . . . . 12  |-  ( (
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  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  j )  e.  {
x  |  ps }
) ) )
5046, 49mpbid 201 . . . . . . . . . . 11  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( j  e.  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  j )  e.  {
x  |  ps }
) )
5150simpld 445 . . . . . . . . . 10  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  j  e.  (
Base `  ( I mPoly  ( Ss  R ) ) ) )
5213, 27rngacl 15417 . . . . . . . . . 10  |-  ( ( ( I mPoly  ( Ss  R ) )  e.  Ring  /\  i  e.  ( Base `  ( I mPoly  ( Ss  R ) ) )  /\  j  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) )  ->  ( i ( +g  `  ( I mPoly 
( Ss  R ) ) ) j )  e.  (
Base `  ( I mPoly  ( Ss  R ) ) ) )
5339, 45, 51, 52syl3anc 1182 . . . . . . . . 9  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( i ( +g  `  ( I mPoly 
( Ss  R ) ) ) j )  e.  (
Base `  ( I mPoly  ( Ss  R ) ) ) )
54 rhmghm 15552 . . . . . . . . . . . . . 14  |-  ( ( ( I evalSub  S ) `
 R )  e.  ( ( I mPoly  ( Ss  R ) ) RingHom  ( S  ^s  ( B  ^m  I
) ) )  -> 
( ( I evalSub  S
) `  R )  e.  ( ( I mPoly  ( Ss  R ) )  GrpHom  ( S  ^s  ( B  ^m  I
) ) ) )
5512, 54syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( I evalSub  S
) `  R )  e.  ( ( I mPoly  ( Ss  R ) )  GrpHom  ( S  ^s  ( B  ^m  I
) ) ) )
5655adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( ( I evalSub  S ) `  R
)  e.  ( ( I mPoly  ( Ss  R ) )  GrpHom  ( S  ^s  ( B  ^m  I ) ) ) )
57 eqid 2316 . . . . . . . . . . . . 13  |-  ( +g  `  ( S  ^s  ( B  ^m  I ) ) )  =  ( +g  `  ( S  ^s  ( B  ^m  I ) ) )
5813, 27, 57ghmlin 14737 . . . . . . . . . . . 12  |-  ( ( ( ( I evalSub  S
) `  R )  e.  ( ( I mPoly  ( Ss  R ) )  GrpHom  ( S  ^s  ( B  ^m  I
) ) )  /\  i  e.  ( Base `  ( I mPoly  ( Ss  R ) ) )  /\  j  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) )  ->  ( ( ( I evalSub  S ) `  R
) `  ( i
( +g  `  ( I mPoly 
( Ss  R ) ) ) j ) )  =  ( ( ( ( I evalSub  S ) `  R
) `  i )
( +g  `  ( S  ^s  ( B  ^m  I
) ) ) ( ( ( I evalSub  S
) `  R ) `  j ) ) )
5956, 45, 51, 58syl3anc 1182 . . . . . . . . . . 11  |-  ( (
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 
( Ss  R ) ) ) j ) )  =  ( ( ( ( I evalSub  S ) `  R
) `  i )
( +g  `  ( S  ^s  ( B  ^m  I
) ) ) ( ( ( I evalSub  S
) `  R ) `  j ) ) )
6031adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  S  e.  CRing )
61 ovex 5925 . . . . . . . . . . . . 13  |-  ( B  ^m  I )  e. 
_V
6261a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( B  ^m  I )  e.  _V )
6316adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( ( I evalSub  S ) `  R
) : ( Base `  ( I mPoly  ( Ss  R ) ) ) --> (
Base `  ( S  ^s  ( B  ^m  I ) ) ) )
64 ffvelrn 5701 . . . . . . . . . . . . 13  |-  ( ( ( ( I evalSub  S
) `  R ) : ( Base `  (
I mPoly  ( Ss  R ) ) ) --> ( Base `  ( S  ^s  ( B  ^m  I ) ) )  /\  i  e.  ( Base `  (
I mPoly  ( Ss  R ) ) ) )  -> 
( ( ( I evalSub  S ) `  R
) `  i )  e.  ( Base `  ( S  ^s  ( B  ^m  I
) ) ) )
6563, 45, 64syl2anc 642 . . . . . . . . . . . 12  |-  ( (
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
) ) ) )
66 ffvelrn 5701 . . . . . . . . . . . . 13  |-  ( ( ( ( I evalSub  S
) `  R ) : ( Base `  (
I mPoly  ( Ss  R ) ) ) --> ( Base `  ( S  ^s  ( B  ^m  I ) ) )  /\  j  e.  ( Base `  (
I mPoly  ( Ss  R ) ) ) )  -> 
( ( ( I evalSub  S ) `  R
) `  j )  e.  ( Base `  ( S  ^s  ( B  ^m  I
) ) ) )
6763, 51, 66syl2anc 642 . . . . . . . . . . . 12  |-  ( (
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
) ) ) )
68 mpfind.cp . . . . . . . . . . . 12  |-  .+  =  ( +g  `  S )
699, 14, 60, 62, 65, 67, 68, 57pwsplusgval 13438 . . . . . . . . . . 11  |-  ( (
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 )  o F 
.+  ( ( ( I evalSub  S ) `  R
) `  j )
) )
7059, 69eqtrd 2348 . . . . . . . . . 10  |-  ( (
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 
( Ss  R ) ) ) j ) )  =  ( ( ( ( I evalSub  S ) `  R
) `  i )  o F  .+  ( ( ( I evalSub  S ) `
 R ) `  j ) ) )
71 simpl 443 . . . . . . . . . . 11  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ph )
7218adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( ( I evalSub  S ) `  R
)  Fn  ( Base `  ( I mPoly  ( Ss  R ) ) ) )
73 fnfvelrn 5700 . . . . . . . . . . . . . 14  |-  ( ( ( ( I evalSub  S
) `  R )  Fn  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  i  e.  ( Base `  (
I mPoly  ( Ss  R ) ) ) )  -> 
( ( ( I evalSub  S ) `  R
) `  i )  e.  ran  ( ( I evalSub  S ) `  R
) )
7472, 45, 73syl2anc 642 . . . . . . . . . . . . 13  |-  ( (
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
) )
7574, 2syl6eleqr 2407 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( ( ( I evalSub  S ) `  R
) `  i )  e.  Q )
7623adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  Fun  ( (
I evalSub  S ) `  R
) )
77 fvimacnvi 5677 . . . . . . . . . . . . 13  |-  ( ( Fun  ( ( I evalSub  S ) `  R
)  /\  i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } ) )  ->  ( ( ( I evalSub  S ) `  R
) `  i )  e.  { x  |  ps } )
7876, 40, 77syl2anc 642 . . . . . . . . . . . 12  |-  ( (
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 } )
7975, 78jca 518 . . . . . . . . . . 11  |-  ( (
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 } ) )
80 fnfvelrn 5700 . . . . . . . . . . . . . 14  |-  ( ( ( ( I evalSub  S
) `  R )  Fn  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  j  e.  ( Base `  (
I mPoly  ( Ss  R ) ) ) )  -> 
( ( ( I evalSub  S ) `  R
) `  j )  e.  ran  ( ( I evalSub  S ) `  R
) )
8172, 51, 80syl2anc 642 . . . . . . . . . . . . 13  |-  ( (
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
) )
8281, 2syl6eleqr 2407 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( ( ( I evalSub  S ) `  R
) `  j )  e.  Q )
83 fvimacnvi 5677 . . . . . . . . . . . . 13  |-  ( ( Fun  ( ( I evalSub  S ) `  R
)  /\  j  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } ) )  ->  ( ( ( I evalSub  S ) `  R
) `  j )  e.  { x  |  ps } )
8476, 46, 83syl2anc 642 . . . . . . . . . . . 12  |-  ( (
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 } )
8582, 84jca 518 . . . . . . . . . . 11  |-  ( (
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 } ) )
86 fvex 5577 . . . . . . . . . . . 12  |-  ( ( ( I evalSub  S ) `
 R ) `  i )  e.  _V
87 fvex 5577 . . . . . . . . . . . 12  |-  ( ( ( I evalSub  S ) `
 R ) `  j )  e.  _V
88 eleq1 2376 . . . . . . . . . . . . . . . 16  |-  ( f  =  ( ( ( I evalSub  S ) `  R
) `  i )  ->  ( f  e.  Q  <->  ( ( ( I evalSub  S
) `  R ) `  i )  e.  Q
) )
89 vex 2825 . . . . . . . . . . . . . . . . . 18  |-  f  e. 
_V
90 mpfind.wc . . . . . . . . . . . . . . . . . 18  |-  ( x  =  f  ->  ( ps 
<->  ta ) )
9189, 90elab 2948 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  { x  |  ps }  <->  ta )
92 eleq1 2376 . . . . . . . . . . . . . . . . 17  |-  ( f  =  ( ( ( I evalSub  S ) `  R
) `  i )  ->  ( f  e.  {
x  |  ps }  <->  ( ( ( I evalSub  S
) `  R ) `  i )  e.  {
x  |  ps }
) )
9391, 92syl5bbr 250 . . . . . . . . . . . . . . . 16  |-  ( f  =  ( ( ( I evalSub  S ) `  R
) `  i )  ->  ( ta  <->  ( (
( I evalSub  S ) `  R ) `  i
)  e.  { x  |  ps } ) )
9488, 93anbi12d 691 . . . . . . . . . . . . . . 15  |-  ( 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 }
) ) )
95 eleq1 2376 . . . . . . . . . . . . . . . 16  |-  ( g  =  ( ( ( I evalSub  S ) `  R
) `  j )  ->  ( g  e.  Q  <->  ( ( ( I evalSub  S
) `  R ) `  j )  e.  Q
) )
96 vex 2825 . . . . . . . . . . . . . . . . . 18  |-  g  e. 
_V
97 mpfind.wd . . . . . . . . . . . . . . . . . 18  |-  ( x  =  g  ->  ( ps 
<->  et ) )
9896, 97elab 2948 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  { x  |  ps }  <->  et )
99 eleq1 2376 . . . . . . . . . . . . . . . . 17  |-  ( g  =  ( ( ( I evalSub  S ) `  R
) `  j )  ->  ( g  e.  {
x  |  ps }  <->  ( ( ( I evalSub  S
) `  R ) `  j )  e.  {
x  |  ps }
) )
10098, 99syl5bbr 250 . . . . . . . . . . . . . . . 16  |-  ( g  =  ( ( ( I evalSub  S ) `  R
) `  j )  ->  ( et  <->  ( (
( I evalSub  S ) `  R ) `  j
)  e.  { x  |  ps } ) )
10195, 100anbi12d 691 . . . . . . . . . . . . . . 15  |-  ( 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 }
) ) )
10294, 101bi2anan9 843 . . . . . . . . . . . . . 14  |-  ( ( 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 } ) ) ) )
103102anbi2d 684 . . . . . . . . . . . . 13  |-  ( ( 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 5925 . . . . . . . . . . . . . . 15  |-  ( f  o F  .+  g
)  e.  _V
105 mpfind.we . . . . . . . . . . . . . . 15  |-  ( x  =  ( f  o F  .+  g )  ->  ( ps  <->  ze )
)
106104, 105elab 2948 . . . . . . . . . . . . . 14  |-  ( ( f  o F  .+  g )  e.  {
x  |  ps }  <->  ze )
107 oveq12 5909 . . . . . . . . . . . . . . 15  |-  ( ( f  =  ( ( ( I evalSub  S ) `
 R ) `  i )  /\  g  =  ( ( ( I evalSub  S ) `  R
) `  j )
)  ->  ( f  o F  .+  g )  =  ( ( ( ( I evalSub  S ) `
 R ) `  i )  o F 
.+  ( ( ( I evalSub  S ) `  R
) `  j )
) )
108107eleq1d 2382 . . . . . . . . . . . . . 14  |-  ( ( f  =  ( ( ( I evalSub  S ) `
 R ) `  i )  /\  g  =  ( ( ( I evalSub  S ) `  R
) `  j )
)  ->  ( (
f  o F  .+  g )  e.  {
x  |  ps }  <->  ( ( ( ( I evalSub  S ) `  R
) `  i )  o F  .+  ( ( ( I evalSub  S ) `
 R ) `  j ) )  e. 
{ x  |  ps } ) )
109106, 108syl5bbr 250 . . . . . . . . . . . . 13  |-  ( ( f  =  ( ( ( I evalSub  S ) `
 R ) `  i )  /\  g  =  ( ( ( I evalSub  S ) `  R
) `  j )
)  ->  ( ze  <->  ( ( ( ( I evalSub  S ) `  R
) `  i )  o F  .+  ( ( ( I evalSub  S ) `
 R ) `  j ) )  e. 
{ x  |  ps } ) )
110103, 109imbi12d 311 . . . . . . . . . . . 12  |-  ( ( 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 )  o F  .+  ( ( ( I evalSub  S ) `
 R ) `  j ) )  e. 
{ x  |  ps } ) ) )
111 mpfind.ad . . . . . . . . . . . 12  |-  ( (
ph  /\  ( (
f  e.  Q  /\  ta )  /\  (
g  e.  Q  /\  et ) ) )  ->  ze )
11286, 87, 110, 111vtocl2 2873 . . . . . . . . . . 11  |-  ( (
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 )  o F 
.+  ( ( ( I evalSub  S ) `  R
) `  j )
)  e.  { x  |  ps } )
11371, 79, 85, 112syl12anc 1180 . . . . . . . . . 10  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( ( ( ( I evalSub  S ) `
 R ) `  i )  o F 
.+  ( ( ( I evalSub  S ) `  R
) `  j )
)  e.  { x  |  ps } )
11470, 113eqeltrd 2390 . . . . . . . . 9  |-  ( (
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 
( Ss  R ) ) ) j ) )  e. 
{ x  |  ps } )
115 elpreima 5683 . . . . . . . . . . 11  |-  ( ( ( I evalSub  S ) `
 R )  Fn  ( Base `  (
I mPoly  ( Ss  R ) ) )  ->  (
( i ( +g  `  ( I mPoly  ( Ss  R ) ) ) j )  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } )  <->  ( (
i ( +g  `  (
I mPoly  ( Ss  R ) ) ) j )  e.  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  ( i ( +g  `  ( I mPoly  ( Ss  R ) ) ) j ) )  e.  {
x  |  ps }
) ) )
11618, 115syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( i ( +g  `  ( I mPoly 
( Ss  R ) ) ) j )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  <->  ( (
i ( +g  `  (
I mPoly  ( Ss  R ) ) ) j )  e.  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  ( i ( +g  `  ( I mPoly  ( Ss  R ) ) ) j ) )  e.  {
x  |  ps }
) ) )
117116adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( ( i ( +g  `  (
I mPoly  ( Ss  R ) ) ) j )  e.  ( `' ( ( I evalSub  S ) `
 R ) " { x  |  ps } )  <->  ( (
i ( +g  `  (
I mPoly  ( Ss  R ) ) ) j )  e.  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  ( i ( +g  `  ( I mPoly  ( Ss  R ) ) ) j ) )  e.  {
x  |  ps }
) ) )
11853, 114, 117mpbir2and 888 . . . . . . . 8  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( i ( +g  `  ( I mPoly 
( Ss  R ) ) ) j )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } ) )
119118adantlr 695 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( Base `  (
I mPoly  ( Ss  R ) ) ) )  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( i ( +g  `  ( I mPoly 
( Ss  R ) ) ) j )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } ) )
12013, 28rngcl 15403 . . . . . . . . . 10  |-  ( ( ( I mPoly  ( Ss  R ) )  e.  Ring  /\  i  e.  ( Base `  ( I mPoly  ( Ss  R ) ) )  /\  j  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) )  ->  ( i ( .r `  ( I mPoly 
( Ss  R ) ) ) j )  e.  (
Base `  ( I mPoly  ( Ss  R ) ) ) )
12139, 45, 51, 120syl3anc 1182 . . . . . . . . 9  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( i ( .r `  ( I mPoly 
( Ss  R ) ) ) j )  e.  (
Base `  ( I mPoly  ( Ss  R ) ) ) )
122 eqid 2316 . . . . . . . . . . . . . . 15  |-  (mulGrp `  ( I mPoly  ( Ss  R
) ) )  =  (mulGrp `  ( I mPoly  ( Ss  R ) ) )
123 eqid 2316 . . . . . . . . . . . . . . 15  |-  (mulGrp `  ( S  ^s  ( B  ^m  I ) ) )  =  (mulGrp `  ( S  ^s  ( B  ^m  I
) ) )
124122, 123rhmmhm 15551 . . . . . . . . . . . . . 14  |-  ( ( ( I evalSub  S ) `
 R )  e.  ( ( I mPoly  ( Ss  R ) ) RingHom  ( S  ^s  ( B  ^m  I
) ) )  -> 
( ( I evalSub  S
) `  R )  e.  ( (mulGrp `  (
I mPoly  ( Ss  R ) ) ) MndHom  (mulGrp `  ( S  ^s  ( B  ^m  I ) ) ) ) )
12512, 124syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( I evalSub  S
) `  R )  e.  ( (mulGrp `  (
I mPoly  ( Ss  R ) ) ) MndHom  (mulGrp `  ( S  ^s  ( B  ^m  I ) ) ) ) )
126125adantr 451 . . . . . . . . . . . 12  |-  ( (
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  ( Ss  R ) ) ) MndHom  (mulGrp `  ( S  ^s  ( B  ^m  I ) ) ) ) )
127122, 13mgpbas 15380 . . . . . . . . . . . . 13  |-  ( Base `  ( I mPoly  ( Ss  R ) ) )  =  ( Base `  (mulGrp `  ( I mPoly  ( Ss  R ) ) ) )
128122, 28mgpplusg 15378 . . . . . . . . . . . . 13  |-  ( .r
`  ( I mPoly  ( Ss  R ) ) )  =  ( +g  `  (mulGrp `  ( I mPoly  ( Ss  R ) ) ) )
129 eqid 2316 . . . . . . . . . . . . . 14  |-  ( .r
`  ( S  ^s  ( B  ^m  I ) ) )  =  ( .r
`  ( S  ^s  ( B  ^m  I ) ) )
130123, 129mgpplusg 15378 . . . . . . . . . . . . 13  |-  ( .r
`  ( S  ^s  ( B  ^m  I ) ) )  =  ( +g  `  (mulGrp `  ( S  ^s  ( B  ^m  I ) ) ) )
131127, 128, 130mhmlin 14471 . . . . . . . . . . . 12  |-  ( ( ( ( I evalSub  S
) `  R )  e.  ( (mulGrp `  (
I mPoly  ( Ss  R ) ) ) MndHom  (mulGrp `  ( S  ^s  ( B  ^m  I ) ) ) )  /\  i  e.  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  j  e.  ( Base `  (
I mPoly  ( Ss  R ) ) ) )  -> 
( ( ( I evalSub  S ) `  R
) `  ( i
( .r `  (
I mPoly  ( Ss  R ) ) ) j ) )  =  ( ( ( ( I evalSub  S
) `  R ) `  i ) ( .r
`  ( S  ^s  ( B  ^m  I ) ) ) ( ( ( I evalSub  S ) `  R
) `  j )
) )
132126, 45, 51, 131syl3anc 1182 . . . . . . . . . . 11  |-  ( (
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  ( Ss  R ) ) ) j ) )  =  ( ( ( ( I evalSub  S
) `  R ) `  i ) ( .r
`  ( S  ^s  ( B  ^m  I ) ) ) ( ( ( I evalSub  S ) `  R
) `  j )
) )
133 mpfind.ct . . . . . . . . . . . 12  |-  .x.  =  ( .r `  S )
1349, 14, 60, 62, 65, 67, 133, 129pwsmulrval 13439 . . . . . . . . . . 11  |-  ( (
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 )  o F 
.x.  ( ( ( I evalSub  S ) `  R
) `  j )
) )
135132, 134eqtrd 2348 . . . . . . . . . 10  |-  ( (
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  ( Ss  R ) ) ) j ) )  =  ( ( ( ( I evalSub  S
) `  R ) `  i )  o F 
.x.  ( ( ( I evalSub  S ) `  R
) `  j )
) )
136 ovex 5925 . . . . . . . . . . . . . . 15  |-  ( f  o F  .x.  g
)  e.  _V
137 mpfind.wf . . . . . . . . . . . . . . 15  |-  ( x  =  ( f  o F  .x.  g )  ->  ( ps  <->  si )
)
138136, 137elab 2948 . . . . . . . . . . . . . 14  |-  ( ( f  o F  .x.  g )  e.  {
x  |  ps }  <->  si )
139 oveq12 5909 . . . . . . . . . . . . . . 15  |-  ( ( f  =  ( ( ( I evalSub  S ) `
 R ) `  i )  /\  g  =  ( ( ( I evalSub  S ) `  R
) `  j )
)  ->  ( f  o F  .x.  g )  =  ( ( ( ( I evalSub  S ) `
 R ) `  i )  o F 
.x.  ( ( ( I evalSub  S ) `  R
) `  j )
) )
140139eleq1d 2382 . . . . . . . . . . . . . 14  |-  ( ( f  =  ( ( ( I evalSub  S ) `
 R ) `  i )  /\  g  =  ( ( ( I evalSub  S ) `  R
) `  j )
)  ->  ( (
f  o F  .x.  g )  e.  {
x  |  ps }  <->  ( ( ( ( I evalSub  S ) `  R
) `  i )  o F  .x.  ( ( ( I evalSub  S ) `
 R ) `  j ) )  e. 
{ x  |  ps } ) )
141138, 140syl5bbr 250 . . . . . . . . . . . . 13  |-  ( ( f  =  ( ( ( I evalSub  S ) `
 R ) `  i )  /\  g  =  ( ( ( I evalSub  S ) `  R
) `  j )
)  ->  ( si  <->  ( ( ( ( I evalSub  S ) `  R
) `  i )  o F  .x.  ( ( ( I evalSub  S ) `
 R ) `  j ) )  e. 
{ x  |  ps } ) )
142103, 141imbi12d 311 . . . . . . . . . . . 12  |-  ( ( 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 )  o F  .x.  ( ( ( I evalSub  S ) `
 R ) `  j ) )  e. 
{ x  |  ps } ) ) )
143 mpfind.mu . . . . . . . . . . . 12  |-  ( (
ph  /\  ( (
f  e.  Q  /\  ta )  /\  (
g  e.  Q  /\  et ) ) )  ->  si )
14486, 87, 142, 143vtocl2 2873 . . . . . . . . . . 11  |-  ( (
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 )  o F 
.x.  ( ( ( I evalSub  S ) `  R
) `  j )
)  e.  { x  |  ps } )
14571, 79, 85, 144syl12anc 1180 . . . . . . . . . 10  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( ( ( ( I evalSub  S ) `
 R ) `  i )  o F 
.x.  ( ( ( I evalSub  S ) `  R
) `  j )
)  e.  { x  |  ps } )
146135, 145eqeltrd 2390 . . . . . . . . 9  |-  ( (
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  ( Ss  R ) ) ) j ) )  e.  { x  |  ps } )
147 elpreima 5683 . . . . . . . . . . 11  |-  ( ( ( I evalSub  S ) `
 R )  Fn  ( Base `  (
I mPoly  ( Ss  R ) ) )  ->  (
( i ( .r
`  ( I mPoly  ( Ss  R ) ) ) j )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  <->  ( (
i ( .r `  ( I mPoly  ( Ss  R
) ) ) j )  e.  ( Base `  ( I mPoly  ( Ss  R ) ) )  /\  ( ( ( I evalSub  S ) `  R
) `  ( i
( .r `  (
I mPoly  ( Ss  R ) ) ) j ) )  e.  { x  |  ps } ) ) )
14818, 147syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( i ( .r `  ( I mPoly 
( Ss  R ) ) ) j )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  <->  ( (
i ( .r `  ( I mPoly  ( Ss  R
) ) ) j )  e.  ( Base `  ( I mPoly  ( Ss  R ) ) )  /\  ( ( ( I evalSub  S ) `  R
) `  ( i
( .r `  (
I mPoly  ( Ss  R ) ) ) j ) )  e.  { x  |  ps } ) ) )
149148adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( ( i ( .r `  (
I mPoly  ( Ss  R ) ) ) j )  e.  ( `' ( ( I evalSub  S ) `
 R ) " { x  |  ps } )  <->  ( (
i ( .r `  ( I mPoly  ( Ss  R
) ) ) j )  e.  ( Base `  ( I mPoly  ( Ss  R ) ) )  /\  ( ( ( I evalSub  S ) `  R
) `  ( i
( .r `  (
I mPoly  ( Ss  R ) ) ) j ) )  e.  { x  |  ps } ) ) )
150121, 146, 149mpbir2and 888 . . . . . . . 8  |-  ( (
ph  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( i ( .r `  ( I mPoly 
( Ss  R ) ) ) j )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } ) )
151150adantlr 695 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( Base `  (
I mPoly  ( Ss  R ) ) ) )  /\  ( i  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  /\  j  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) ) )  ->  ( i ( .r `  ( I mPoly 
( Ss  R ) ) ) j )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } ) )
1527mplassa 16247 . . . . . . . . . . . . . 14  |-  ( ( I  e.  _V  /\  ( Ss  R )  e.  CRing )  ->  ( I mPoly  ( Ss  R ) )  e. AssAlg
)
15330, 34, 152syl2anc 642 . . . . . . . . . . . . 13  |-  ( ph  ->  ( I mPoly  ( Ss  R ) )  e. AssAlg )
154 eqid 2316 . . . . . . . . . . . . . 14  |-  (Scalar `  ( I mPoly  ( Ss  R
) ) )  =  (Scalar `  ( I mPoly  ( Ss  R ) ) )
15529, 154asclrhm 16130 . . . . . . . . . . . . 13  |-  ( ( I mPoly  ( Ss  R ) )  e. AssAlg  ->  (algSc `  ( I mPoly  ( Ss  R
) ) )  e.  ( (Scalar `  (
I mPoly  ( Ss  R ) ) ) RingHom  ( I mPoly 
( Ss  R ) ) ) )
156153, 155syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  (algSc `  ( I mPoly  ( Ss  R ) ) )  e.  ( (Scalar `  ( I mPoly  ( Ss  R
) ) ) RingHom  (
I mPoly  ( Ss  R ) ) ) )
157 eqid 2316 . . . . . . . . . . . . 13  |-  ( Base `  (Scalar `  ( I mPoly  ( Ss  R ) ) ) )  =  ( Base `  (Scalar `  ( I mPoly  ( Ss  R ) ) ) )
158157, 13rhmf 15553 . . . . . . . . . . . 12  |-  ( (algSc `  ( I mPoly  ( Ss  R ) ) )  e.  ( (Scalar `  (
I mPoly  ( Ss  R ) ) ) RingHom  ( I mPoly 
( Ss  R ) ) )  ->  (algSc `  (
I mPoly  ( Ss  R ) ) ) : (
Base `  (Scalar `  (
I mPoly  ( Ss  R ) ) ) ) --> (
Base `  ( I mPoly  ( Ss  R ) ) ) )
159156, 158syl 15 . . . . . . . . . . 11  |-  ( ph  ->  (algSc `  ( I mPoly  ( Ss  R ) ) ) : ( Base `  (Scalar `  ( I mPoly  ( Ss  R ) ) ) ) --> ( Base `  (
I mPoly  ( Ss  R ) ) ) )
160159adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( Base `  ( Ss  R
) ) )  -> 
(algSc `  ( I mPoly  ( Ss  R ) ) ) : ( Base `  (Scalar `  ( I mPoly  ( Ss  R ) ) ) ) --> ( Base `  (
I mPoly  ( Ss  R ) ) ) )
1617, 30, 34mplsca 16238 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Ss  R )  =  (Scalar `  ( I mPoly  ( Ss  R ) ) ) )
162161fveq2d 5567 . . . . . . . . . . . 12  |-  ( ph  ->  ( Base `  ( Ss  R ) )  =  ( Base `  (Scalar `  ( I mPoly  ( Ss  R ) ) ) ) )
163162eleq2d 2383 . . . . . . . . . . 11  |-  ( ph  ->  ( i  e.  (
Base `  ( Ss  R
) )  <->  i  e.  ( Base `  (Scalar `  (
I mPoly  ( Ss  R ) ) ) ) ) )
164163biimpa 470 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( Base `  ( Ss  R
) ) )  -> 
i  e.  ( Base `  (Scalar `  ( I mPoly  ( Ss  R ) ) ) ) )
165 ffvelrn 5701 . . . . . . . . . 10  |-  ( ( (algSc `  ( I mPoly  ( Ss  R ) ) ) : ( Base `  (Scalar `  ( I mPoly  ( Ss  R ) ) ) ) --> ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  i  e.  ( Base `  (Scalar `  ( I mPoly  ( Ss  R ) ) ) ) )  ->  ( (algSc `  ( I mPoly  ( Ss  R ) ) ) `  i )  e.  (
Base `  ( I mPoly  ( Ss  R ) ) ) )
166160, 164, 165syl2anc 642 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( Base `  ( Ss  R
) ) )  -> 
( (algSc `  (
I mPoly  ( Ss  R ) ) ) `  i
)  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) )
16730adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( Base `  ( Ss  R
) ) )  ->  I  e.  _V )
16831adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( Base `  ( Ss  R
) ) )  ->  S  e.  CRing )
16932adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( Base `  ( Ss  R
) ) )  ->  R  e.  (SubRing `  S
) )
17010subrgss 15595 . . . . . . . . . . . . . . 15  |-  ( R  e.  (SubRing `  S
)  ->  R  C_  B
)
17132, 170syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  R  C_  B )
1728, 10ressbas2 13246 . . . . . . . . . . . . . 14  |-  ( R 
C_  B  ->  R  =  ( Base `  ( Ss  R ) ) )
173171, 172syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  R  =  ( Base `  ( Ss  R ) ) )
174173eleq2d 2383 . . . . . . . . . . . 12  |-  ( ph  ->  ( i  e.  R  <->  i  e.  ( Base `  ( Ss  R ) ) ) )
175174biimpar 471 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( Base `  ( Ss  R
) ) )  -> 
i  e.  R )
1766, 7, 8, 10, 29, 167, 168, 169, 175evlssca 19459 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( Base `  ( Ss  R
) ) )  -> 
( ( ( I evalSub  S ) `  R
) `  ( (algSc `  ( I mPoly  ( Ss  R ) ) ) `  i ) )  =  ( ( B  ^m  I )  X.  {
i } ) )
177 mpfind.co . . . . . . . . . . . . . 14  |-  ( (
ph  /\  f  e.  R )  ->  ch )
178177ralrimiva 2660 . . . . . . . . . . . . 13  |-  ( ph  ->  A. f  e.  R  ch )
179 snex 4253 . . . . . . . . . . . . . . . . 17  |-  { f }  e.  _V
18061, 179xpex 4838 . . . . . . . . . . . . . . . 16  |-  ( ( B  ^m  I )  X.  { f } )  e.  _V
181 mpfind.wa . . . . . . . . . . . . . . . 16  |-  ( x  =  ( ( B  ^m  I )  X. 
{ f } )  ->  ( ps  <->  ch )
)
182180, 181elab 2948 . . . . . . . . . . . . . . 15  |-  ( ( ( B  ^m  I
)  X.  { f } )  e.  {
x  |  ps }  <->  ch )
183 sneq 3685 . . . . . . . . . . . . . . . . 17  |-  ( f  =  i  ->  { f }  =  { i } )
184183xpeq2d 4750 . . . . . . . . . . . . . . . 16  |-  ( f  =  i  ->  (
( B  ^m  I
)  X.  { f } )  =  ( ( B  ^m  I
)  X.  { i } ) )
185184eleq1d 2382 . . . . . . . . . . . . . . 15  |-  ( f  =  i  ->  (
( ( B  ^m  I )  X.  {
f } )  e. 
{ x  |  ps } 
<->  ( ( B  ^m  I )  X.  {
i } )  e. 
{ x  |  ps } ) )
186182, 185syl5bbr 250 . . . . . . . . . . . . . 14  |-  ( f  =  i  ->  ( ch 
<->  ( ( B  ^m  I )  X.  {
i } )  e. 
{ x  |  ps } ) )
187186cbvralv 2798 . . . . . . . . . . . . 13  |-  ( A. f  e.  R  ch  <->  A. i  e.  R  ( ( B  ^m  I
)  X.  { i } )  e.  {
x  |  ps }
)
188178, 187sylib 188 . . . . . . . . . . . 12  |-  ( ph  ->  A. i  e.  R  ( ( B  ^m  I )  X.  {
i } )  e. 
{ x  |  ps } )
189188r19.21bi 2675 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  R )  ->  (
( B  ^m  I
)  X.  { i } )  e.  {
x  |  ps }
)
190175, 189syldan 456 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( Base `  ( Ss  R
) ) )  -> 
( ( B  ^m  I )  X.  {
i } )  e. 
{ x  |  ps } )
191176, 190eqeltrd 2390 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( Base `  ( Ss  R
) ) )  -> 
( ( ( I evalSub  S ) `  R
) `  ( (algSc `  ( I mPoly  ( Ss  R ) ) ) `  i ) )  e. 
{ x  |  ps } )
192 elpreima 5683 . . . . . . . . . . 11  |-  ( ( ( I evalSub  S ) `
 R )  Fn  ( Base `  (
I mPoly  ( Ss  R ) ) )  ->  (
( (algSc `  (
I mPoly  ( Ss  R ) ) ) `  i
)  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } )  <->  ( (
(algSc `  ( I mPoly  ( Ss  R ) ) ) `
 i )  e.  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  ( (algSc `  (
I mPoly  ( Ss  R ) ) ) `  i
) )  e.  {
x  |  ps }
) ) )
19318, 192syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( (algSc `  ( I mPoly  ( Ss  R
) ) ) `  i )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  <->  ( (
(algSc `  ( I mPoly  ( Ss  R ) ) ) `
 i )  e.  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  ( (algSc `  (
I mPoly  ( Ss  R ) ) ) `  i
) )  e.  {
x  |  ps }
) ) )
194193adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( Base `  ( Ss  R
) ) )  -> 
( ( (algSc `  ( I mPoly  ( Ss  R
) ) ) `  i )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  <->  ( (
(algSc `  ( I mPoly  ( Ss  R ) ) ) `
 i )  e.  ( Base `  (
I mPoly  ( Ss  R ) ) )  /\  (
( ( I evalSub  S
) `  R ) `  ( (algSc `  (
I mPoly  ( Ss  R ) ) ) `  i
) )  e.  {
x  |  ps }
) ) )
195166, 191, 194mpbir2and 888 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( Base `  ( Ss  R
) ) )  -> 
( (algSc `  (
I mPoly  ( Ss  R ) ) ) `  i
)  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) )
196195adantlr 695 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( Base `  (
I mPoly  ( Ss  R ) ) ) )  /\  i  e.  ( Base `  ( Ss  R ) ) )  ->  ( (algSc `  ( I mPoly  ( Ss  R
) ) ) `  i )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } ) )
19730adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  I )  ->  I  e.  _V )
19836adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  I )  ->  ( Ss  R )  e.  Ring )
199 simpr 447 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  I )  ->  i  e.  I )
2007, 26, 13, 197, 198, 199mvrcl 16242 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  I )  ->  (
( I mVar  ( Ss  R ) ) `  i
)  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) )
20131adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  I )  ->  S  e.  CRing )
20232adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  I )  ->  R  e.  (SubRing `  S )
)
2036, 26, 8, 10, 197, 201, 202, 199evlsvar 19460 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  I )  ->  (
( ( I evalSub  S
) `  R ) `  ( ( I mVar  ( Ss  R ) ) `  i ) )  =  ( g  e.  ( B  ^m  I ) 
|->  ( g `  i
) ) )
204 mpfind.pr . . . . . . . . . . . . . 14  |-  ( (
ph  /\  f  e.  I )  ->  th )
20561mptex 5787 . . . . . . . . . . . . . . 15  |-  ( g  e.  ( B  ^m  I )  |->  ( g `
 f ) )  e.  _V
206 mpfind.wb . . . . . . . . . . . . . . 15  |-  ( x  =  ( g  e.  ( B  ^m  I
)  |->  ( g `  f ) )  -> 
( ps  <->  th )
)
207205, 206elab 2948 . . . . . . . . . . . . . 14  |-  ( ( g  e.  ( B  ^m  I )  |->  ( g `  f ) )  e.  { x  |  ps }  <->  th )
208204, 207sylibr 203 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  I )  ->  (
g  e.  ( B  ^m  I )  |->  ( g `  f ) )  e.  { x  |  ps } )
209208ralrimiva 2660 . . . . . . . . . . . 12  |-  ( ph  ->  A. f  e.  I 
( g  e.  ( B  ^m  I ) 
|->  ( g `  f
) )  e.  {
x  |  ps }
)
210 fveq2 5563 . . . . . . . . . . . . . . 15  |-  ( f  =  i  ->  (
g `  f )  =  ( g `  i ) )
211210mpteq2dv 4144 . . . . . . . . . . . . . 14  |-  ( f  =  i  ->  (
g  e.  ( B  ^m  I )  |->  ( g `  f ) )  =  ( g  e.  ( B  ^m  I )  |->  ( g `
 i ) ) )
212211eleq1d 2382 . . . . . . . . . . . . 13  |-  ( f  =  i  ->  (
( g  e.  ( B  ^m  I ) 
|->  ( g `  f
) )  e.  {
x  |  ps }  <->  ( g  e.  ( B  ^m  I )  |->  ( g `  i ) )  e.  { x  |  ps } ) )
213212cbvralv 2798 . . . . . . . . . . . 12  |-  ( 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 } )
214209, 213sylib 188 . . . . . . . . . . 11  |-  ( ph  ->  A. i  e.  I 
( g  e.  ( B  ^m  I ) 
|->  ( g `  i
) )  e.  {
x  |  ps }
)
215214r19.21bi 2675 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  I )  ->  (
g  e.  ( B  ^m  I )  |->  ( g `  i ) )  e.  { x  |  ps } )
216203, 215eqeltrd 2390 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  I )  ->  (
( ( I evalSub  S
) `  R ) `  ( ( I mVar  ( Ss  R ) ) `  i ) )  e. 
{ x  |  ps } )
217 elpreima 5683 . . . . . . . . . . 11  |-  ( ( ( I evalSub  S ) `
 R )  Fn  ( Base `  (
I mPoly  ( Ss  R ) ) )  ->  (
( ( I mVar  ( Ss  R ) ) `  i )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  <->  ( (
( I mVar  ( Ss  R ) ) `  i
)  e.  ( Base `  ( I mPoly  ( Ss  R ) ) )  /\  ( ( ( I evalSub  S ) `  R
) `  ( (
I mVar  ( Ss  R ) ) `  i ) )  e.  { x  |  ps } ) ) )
21818, 217syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( I mVar  ( Ss  R ) ) `  i )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  <->  ( (
( I mVar  ( Ss  R ) ) `  i
)  e.  ( Base `  ( I mPoly  ( Ss  R ) ) )  /\  ( ( ( I evalSub  S ) `  R
) `  ( (
I mVar  ( Ss  R ) ) `  i ) )  e.  { x  |  ps } ) ) )
219218adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  I )  ->  (
( ( I mVar  ( Ss  R ) ) `  i )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } )  <->  ( (
( I mVar  ( Ss  R ) ) `  i
)  e.  ( Base `  ( I mPoly  ( Ss  R ) ) )  /\  ( ( ( I evalSub  S ) `  R
) `  ( (
I mVar  ( Ss  R ) ) `  i ) )  e.  { x  |  ps } ) ) )
220200, 216, 219mpbir2and 888 . . . . . . . 8  |-  ( (
ph  /\  i  e.  I )  ->  (
( I mVar  ( Ss  R ) ) `  i
)  e.  ( `' ( ( I evalSub  S
) `  R ) " { x  |  ps } ) )
221220adantlr 695 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( Base `  (
I mPoly  ( Ss  R ) ) ) )  /\  i  e.  I )  ->  ( ( I mVar  ( Ss  R ) ) `  i )  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } ) )
222 simpr 447 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) )  ->  y  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) )
22330adantr 451 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) )  ->  I  e.  _V )
22434adantr 451 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) )  ->  ( Ss  R
)  e.  CRing )
22525, 26, 7, 27, 28, 29, 13, 119, 151, 196, 221, 222, 223, 224mplind 16292 . . . . . 6  |-  ( (
ph  /\  y  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) )  ->  y  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } ) )
226 fvimacnvi 5677 . . . . . 6  |-  ( ( Fun  ( ( I evalSub  S ) `  R
)  /\  y  e.  ( `' ( ( I evalSub  S ) `  R
) " { x  |  ps } ) )  ->  ( ( ( I evalSub  S ) `  R
) `  y )  e.  { x  |  ps } )
22724, 225, 226syl2anc 642 . . . . 5  |-  ( (
ph  /\  y  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) )  ->  ( (
( I evalSub  S ) `  R ) `  y
)  e.  { x  |  ps } )
228 eleq1 2376 . . . . 5  |-  ( ( ( ( I evalSub  S
) `  R ) `  y )  =  A  ->  ( ( ( ( I evalSub  S ) `
 R ) `  y )  e.  {
x  |  ps }  <->  A  e.  { x  |  ps } ) )
229227, 228syl5ibcom 211 . . . 4  |-  ( (
ph  /\  y  e.  ( Base `  ( I mPoly  ( Ss  R ) ) ) )  ->  ( (
( ( I evalSub  S
) `  R ) `  y )  =  A  ->  A  e.  {
x  |  ps }
) )
230229rexlimdva 2701 . . 3  |-  ( ph  ->  ( E. y  e.  ( Base `  (
I mPoly  ( Ss  R ) ) ) ( ( ( I evalSub  S ) `
 R ) `  y )  =  A  ->  A  e.  {
x  |  ps }
) )
23121, 230mpd 14 . 2  |-  ( ph  ->  A  e.  { x  |  ps } )
232 mpfind.wg . . . 4  |-  ( x  =  A  ->  ( ps 
<->  rh ) )
233232elabg 2949 . . 3  |-  ( A  e.  Q  ->  ( A  e.  { x  |  ps }  <->  rh )
)
2341, 233syl 15 . 2  |-  ( ph  ->  ( A  e.  {
x  |  ps }  <->  rh ) )
235231, 234mpbid 201 1  |-  ( ph  ->  rh )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1633    e. wcel 1701   {cab 2302   A.wral 2577   E.wrex 2578   _Vcvv 2822    C_ wss 3186   {csn 3674    e. cmpt 4114    X. cxp 4724   `'ccnv 4725   ran crn 4727   "cima 4729   Fun wfun 5286    Fn wfn 5287   -->wf 5288   ` cfv 5292  (class class class)co 5900    o Fcof 6118    ^m cmap 6815   Basecbs 13195   ↾s cress 13196   +g cplusg 13255   .rcmulr 13256  Scalarcsca 13258    ^s cpws 13396   MndHom cmhm 14462    GrpHom cghm 14729  mulGrpcmgp 15374   Ringcrg 15386   CRingccrg 15387   RingHom crh 15543  SubRingcsubrg 15590  AssAlgcasa 16099  algSccascl 16101   mVar cmvr 16137   mPoly cmpl 16138   evalSub ces 16139
This theorem is referenced by:  pf1ind  19491  mzpmfp  25973
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-inf2 7387  ax-cnex 8838  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rmo 2585  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-int 3900  df-iun 3944  df-iin 3945  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-se 4390  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-isom 5301  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-of 6120  df-ofr 6121  df-1st 6164  df-2nd 6165  df-riota 6346  df-recs 6430  df-rdg 6465  df-1o 6521  df-2o 6522  df-oadd 6525  df-er 6702  df-map 6817  df-pm 6818  df-ixp 6861  df-en 6907  df-dom 6908  df-sdom 6909  df-fin 6910  df-sup 7239  df-oi 7270  df-card 7617  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-nn 9792  df-2 9849  df-3 9850  df-4 9851  df-5 9852  df-6 9853  df-7 9854  df-8 9855  df-9 9856  df-10 9857  df-n0 10013  df-z 10072  df-dec 10172  df-uz 10278  df-fz 10830  df-fzo 10918  df-seq 11094  df-hash 11385  df-struct 13197  df-ndx 13198  df-slot 13199  df-base 13200  df-sets 13201  df-ress 13202  df-plusg 13268  df-mulr 13269  df-sca 13271  df-vsca 13272  df-tset 13274  df-ple 13275  df-ds 13277  df-hom 13279  df-cco 13280  df-prds 13397  df-pws 13399  df-0g 13453  df-gsum 13454  df-mre 13537  df-mrc 13538  df-acs 13540  df-mnd 14416  df-mhm 14464  df-submnd 14465  df-grp 14538  df-minusg 14539  df-sbg 14540  df-mulg 14541  df-subg 14667  df-ghm 14730  df-cntz 14842  df-cmn 15140  df-abl 15141  df-mgp 15375  df-rng 15389  df-cring 15390  df-ur 15391  df-rnghom 15545  df-subrg 15592  df-lmod 15678  df-lss 15739  df-lsp 15778  df-assa 16102  df-asp 16103  df-ascl 16104  df-psr 16147  df-mvr 16148  df-mpl 16149  df-evls 16150
  Copyright terms: Public domain W3C validator