Metamath Proof Explorer

Theorem eldioph2

Description: Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 . (Contributed by Stefan O'Rear, 8-Oct-2014) (Revised by Stefan O'Rear, 5-Jun-2015)

Ref Expression
Assertion eldioph2 
|- ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ P e. ( mzPoly ` S ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 mzpcompact2 
 |-  ( P e. ( mzPoly ` S ) -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ S /\ P = ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ) )
2 1 3ad2ant3 
 |-  ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ P e. ( mzPoly ` S ) ) -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ S /\ P = ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ) )
3 fveq1 
 |-  ( P = ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) -> ( P ` u ) = ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) )
4 3 eqeq1d 
 |-  ( P = ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) -> ( ( P ` u ) = 0 <-> ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) )
5 4 anbi2d 
 |-  ( P = ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) -> ( ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) <-> ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) ) )
6 5 rexbidv 
 |-  ( P = ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) -> ( E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) <-> E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) ) )
7 6 abbidv 
 |-  ( P = ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) } )
8 7 ad2antll 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ P e. ( mzPoly ` S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ ( a C_ S /\ P = ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) } )
9 simplll 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) -> N e. NN0 )
10 simplrl 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) -> a e. Fin )
11 fzfi 
 |-  ( 1 ... N ) e. Fin
12 unfi 
 |-  ( ( a e. Fin /\ ( 1 ... N ) e. Fin ) -> ( a u. ( 1 ... N ) ) e. Fin )
13 10 11 12 sylancl 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) -> ( a u. ( 1 ... N ) ) e. Fin )
14 ssun2 
 |-  ( 1 ... N ) C_ ( a u. ( 1 ... N ) )
15 14 a1i 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) -> ( 1 ... N ) C_ ( a u. ( 1 ... N ) ) )
16 eldioph2lem1 
 |-  ( ( N e. NN0 /\ ( a u. ( 1 ... N ) ) e. Fin /\ ( 1 ... N ) C_ ( a u. ( 1 ... N ) ) ) -> E. c e. ( ZZ>= ` N ) E. d e. _V ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
17 9 13 15 16 syl3anc 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) -> E. c e. ( ZZ>= ` N ) E. d e. _V ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
18 f1ococnv2 
 |-  ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) -> ( d o. `' d ) = ( _I |` ( a u. ( 1 ... N ) ) ) )
19 18 ad2antrl 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( d o. `' d ) = ( _I |` ( a u. ( 1 ... N ) ) ) )
20 19 reseq1d 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( ( d o. `' d ) |` a ) = ( ( _I |` ( a u. ( 1 ... N ) ) ) |` a ) )
21 ssun1 
 |-  a C_ ( a u. ( 1 ... N ) )
22 resabs1 
 |-  ( a C_ ( a u. ( 1 ... N ) ) -> ( ( _I |` ( a u. ( 1 ... N ) ) ) |` a ) = ( _I |` a ) )
23 21 22 ax-mp 
 |-  ( ( _I |` ( a u. ( 1 ... N ) ) ) |` a ) = ( _I |` a )
24 20 23 eqtr2di 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( _I |` a ) = ( ( d o. `' d ) |` a ) )
25 resco 
 |-  ( ( d o. `' d ) |` a ) = ( d o. ( `' d |` a ) )
26 24 25 eqtrdi 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( _I |` a ) = ( d o. ( `' d |` a ) ) )
27 26 adantr 
 |-  ( ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) /\ e e. ( ZZ ^m S ) ) -> ( _I |` a ) = ( d o. ( `' d |` a ) ) )
28 27 coeq2d 
 |-  ( ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) /\ e e. ( ZZ ^m S ) ) -> ( e o. ( _I |` a ) ) = ( e o. ( d o. ( `' d |` a ) ) ) )
29 coires1 
 |-  ( e o. ( _I |` a ) ) = ( e |` a )
30 coass 
 |-  ( ( e o. d ) o. ( `' d |` a ) ) = ( e o. ( d o. ( `' d |` a ) ) )
31 30 eqcomi 
 |-  ( e o. ( d o. ( `' d |` a ) ) ) = ( ( e o. d ) o. ( `' d |` a ) )
32 28 29 31 3eqtr3g 
 |-  ( ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) /\ e e. ( ZZ ^m S ) ) -> ( e |` a ) = ( ( e o. d ) o. ( `' d |` a ) ) )
33 32 fveq2d 
 |-  ( ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) /\ e e. ( ZZ ^m S ) ) -> ( b ` ( e |` a ) ) = ( b ` ( ( e o. d ) o. ( `' d |` a ) ) ) )
34 ovexd 
 |-  ( ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) /\ e e. ( ZZ ^m S ) ) -> ( 1 ... c ) e. _V )
35 simpr 
 |-  ( ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) /\ e e. ( ZZ ^m S ) ) -> e e. ( ZZ ^m S ) )
36 f1of1 
 |-  ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) -> d : ( 1 ... c ) -1-1-> ( a u. ( 1 ... N ) ) )
37 36 ad2antrl 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> d : ( 1 ... c ) -1-1-> ( a u. ( 1 ... N ) ) )
38 simpr 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) -> a C_ S )
39 simprr 
 |-  ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) -> ( 1 ... N ) C_ S )
40 39 ad2antrr 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) -> ( 1 ... N ) C_ S )
41 38 40 unssd 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) -> ( a u. ( 1 ... N ) ) C_ S )
42 41 ad2antrr 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( a u. ( 1 ... N ) ) C_ S )
43 f1ss 
 |-  ( ( d : ( 1 ... c ) -1-1-> ( a u. ( 1 ... N ) ) /\ ( a u. ( 1 ... N ) ) C_ S ) -> d : ( 1 ... c ) -1-1-> S )
44 37 42 43 syl2anc 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> d : ( 1 ... c ) -1-1-> S )
45 f1f 
 |-  ( d : ( 1 ... c ) -1-1-> S -> d : ( 1 ... c ) --> S )
46 44 45 syl 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> d : ( 1 ... c ) --> S )
47 46 adantr 
 |-  ( ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) /\ e e. ( ZZ ^m S ) ) -> d : ( 1 ... c ) --> S )
48 mapco2g 
 |-  ( ( ( 1 ... c ) e. _V /\ e e. ( ZZ ^m S ) /\ d : ( 1 ... c ) --> S ) -> ( e o. d ) e. ( ZZ ^m ( 1 ... c ) ) )
49 34 35 47 48 syl3anc 
 |-  ( ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) /\ e e. ( ZZ ^m S ) ) -> ( e o. d ) e. ( ZZ ^m ( 1 ... c ) ) )
50 coeq1 
 |-  ( h = ( e o. d ) -> ( h o. ( `' d |` a ) ) = ( ( e o. d ) o. ( `' d |` a ) ) )
51 50 fveq2d 
 |-  ( h = ( e o. d ) -> ( b ` ( h o. ( `' d |` a ) ) ) = ( b ` ( ( e o. d ) o. ( `' d |` a ) ) ) )
52 eqid 
 |-  ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) = ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) )
53 fvex 
 |-  ( b ` ( ( e o. d ) o. ( `' d |` a ) ) ) e. _V
54 51 52 53 fvmpt 
 |-  ( ( e o. d ) e. ( ZZ ^m ( 1 ... c ) ) -> ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` ( e o. d ) ) = ( b ` ( ( e o. d ) o. ( `' d |` a ) ) ) )
55 49 54 syl 
 |-  ( ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) /\ e e. ( ZZ ^m S ) ) -> ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` ( e o. d ) ) = ( b ` ( ( e o. d ) o. ( `' d |` a ) ) ) )
56 33 55 eqtr4d 
 |-  ( ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) /\ e e. ( ZZ ^m S ) ) -> ( b ` ( e |` a ) ) = ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` ( e o. d ) ) )
57 56 mpteq2dva 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) = ( e e. ( ZZ ^m S ) |-> ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` ( e o. d ) ) ) )
58 57 fveq1d 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = ( ( e e. ( ZZ ^m S ) |-> ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` ( e o. d ) ) ) ` u ) )
59 58 eqeq1d 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 <-> ( ( e e. ( ZZ ^m S ) |-> ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` ( e o. d ) ) ) ` u ) = 0 ) )
60 59 anbi2d 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) <-> ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` ( e o. d ) ) ) ` u ) = 0 ) ) )
61 60 rexbidv 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) <-> E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` ( e o. d ) ) ) ` u ) = 0 ) ) )
62 61 abbidv 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` ( e o. d ) ) ) ` u ) = 0 ) } )
63 simplrl 
 |-  ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) -> S e. _V )
64 63 ad3antrrr 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> S e. _V )
65 simprr 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) )
66 diophrw 
 |-  ( ( S e. _V /\ d : ( 1 ... c ) -1-1-> S /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` ( e o. d ) ) ) ` u ) = 0 ) } = { t | E. g e. ( NN0 ^m ( 1 ... c ) ) ( t = ( g |` ( 1 ... N ) ) /\ ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` g ) = 0 ) } )
67 64 44 65 66 syl3anc 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` ( e o. d ) ) ) ` u ) = 0 ) } = { t | E. g e. ( NN0 ^m ( 1 ... c ) ) ( t = ( g |` ( 1 ... N ) ) /\ ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` g ) = 0 ) } )
68 62 67 eqtrd 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) } = { t | E. g e. ( NN0 ^m ( 1 ... c ) ) ( t = ( g |` ( 1 ... N ) ) /\ ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` g ) = 0 ) } )
69 simp-5l 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> N e. NN0 )
70 simplrl 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> c e. ( ZZ>= ` N ) )
71 ovexd 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( 1 ... c ) e. _V )
72 simplrr 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) -> b e. ( mzPoly ` a ) )
73 72 ad2antrr 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> b e. ( mzPoly ` a ) )
74 f1ocnv 
 |-  ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) -> `' d : ( a u. ( 1 ... N ) ) -1-1-onto-> ( 1 ... c ) )
75 f1of 
 |-  ( `' d : ( a u. ( 1 ... N ) ) -1-1-onto-> ( 1 ... c ) -> `' d : ( a u. ( 1 ... N ) ) --> ( 1 ... c ) )
76 74 75 syl 
 |-  ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) -> `' d : ( a u. ( 1 ... N ) ) --> ( 1 ... c ) )
77 fssres 
 |-  ( ( `' d : ( a u. ( 1 ... N ) ) --> ( 1 ... c ) /\ a C_ ( a u. ( 1 ... N ) ) ) -> ( `' d |` a ) : a --> ( 1 ... c ) )
78 76 21 77 sylancl 
 |-  ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) -> ( `' d |` a ) : a --> ( 1 ... c ) )
79 78 ad2antrl 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( `' d |` a ) : a --> ( 1 ... c ) )
80 mzprename 
 |-  ( ( ( 1 ... c ) e. _V /\ b e. ( mzPoly ` a ) /\ ( `' d |` a ) : a --> ( 1 ... c ) ) -> ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) e. ( mzPoly ` ( 1 ... c ) ) )
81 71 73 79 80 syl3anc 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) e. ( mzPoly ` ( 1 ... c ) ) )
82 eldioph 
 |-  ( ( N e. NN0 /\ c e. ( ZZ>= ` N ) /\ ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) e. ( mzPoly ` ( 1 ... c ) ) ) -> { t | E. g e. ( NN0 ^m ( 1 ... c ) ) ( t = ( g |` ( 1 ... N ) ) /\ ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` g ) = 0 ) } e. ( Dioph ` N ) )
83 69 70 81 82 syl3anc 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> { t | E. g e. ( NN0 ^m ( 1 ... c ) ) ( t = ( g |` ( 1 ... N ) ) /\ ( ( h e. ( ZZ ^m ( 1 ... c ) ) |-> ( b ` ( h o. ( `' d |` a ) ) ) ) ` g ) = 0 ) } e. ( Dioph ` N ) )
84 68 83 eqeltrd 
 |-  ( ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) /\ ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) } e. ( Dioph ` N ) )
85 84 ex 
 |-  ( ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) /\ ( c e. ( ZZ>= ` N ) /\ d e. _V ) ) -> ( ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) } e. ( Dioph ` N ) ) )
86 85 rexlimdvva 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) -> ( E. c e. ( ZZ>= ` N ) E. d e. _V ( d : ( 1 ... c ) -1-1-onto-> ( a u. ( 1 ... N ) ) /\ ( d |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) } e. ( Dioph ` N ) ) )
87 17 86 mpd 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) } e. ( Dioph ` N ) )
88 87 exp31 
 |-  ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) ) -> ( ( a e. Fin /\ b e. ( mzPoly ` a ) ) -> ( a C_ S -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) } e. ( Dioph ` N ) ) ) )
89 88 3adant3 
 |-  ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ P e. ( mzPoly ` S ) ) -> ( ( a e. Fin /\ b e. ( mzPoly ` a ) ) -> ( a C_ S -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) } e. ( Dioph ` N ) ) ) )
90 89 imp31 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ P e. ( mzPoly ` S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ a C_ S ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) } e. ( Dioph ` N ) )
91 90 adantrr 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ P e. ( mzPoly ` S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ ( a C_ S /\ P = ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ` u ) = 0 ) } e. ( Dioph ` N ) )
92 8 91 eqeltrd 
 |-  ( ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ P e. ( mzPoly ` S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) /\ ( a C_ S /\ P = ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. ( Dioph ` N ) )
93 92 ex 
 |-  ( ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ P e. ( mzPoly ` S ) ) /\ ( a e. Fin /\ b e. ( mzPoly ` a ) ) ) -> ( ( a C_ S /\ P = ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. ( Dioph ` N ) ) )
94 93 rexlimdvva 
 |-  ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ P e. ( mzPoly ` S ) ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ S /\ P = ( e e. ( ZZ ^m S ) |-> ( b ` ( e |` a ) ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. ( Dioph ` N ) ) )
95 2 94 mpd 
 |-  ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ P e. ( mzPoly ` S ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. ( Dioph ` N ) )