Metamath Proof Explorer

Theorem diophren

Description: Change variables in a Diophantine set, using class notation. This allows already proved Diophantine sets to be reused in contexts with more variables. (Contributed by Stefan O'Rear, 16-Oct-2014) (Revised by Stefan O'Rear, 5-Jun-2015)

Ref Expression
Assertion diophren 
|- ( ( S e. ( Dioph ` N ) /\ M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. S } e. ( Dioph ` M ) )

Proof

Step Hyp Ref Expression
1 zex 
 |-  ZZ e. _V
2 difexg 
 |-  ( ZZ e. _V -> ( ZZ \ NN ) e. _V )
3 1 2 ax-mp 
 |-  ( ZZ \ NN ) e. _V
4 ominf 
 |-  -. _om e. Fin
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 0p1e1 
 |-  ( 0 + 1 ) = 1
7 6 fveq2i 
 |-  ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
8 5 7 eqtr4i 
 |-  NN = ( ZZ>= ` ( 0 + 1 ) )
9 8 difeq2i 
 |-  ( ZZ \ NN ) = ( ZZ \ ( ZZ>= ` ( 0 + 1 ) ) )
10 0z 
 |-  0 e. ZZ
11 lzenom 
 |-  ( 0 e. ZZ -> ( ZZ \ ( ZZ>= ` ( 0 + 1 ) ) ) ~~ _om )
12 10 11 ax-mp 
 |-  ( ZZ \ ( ZZ>= ` ( 0 + 1 ) ) ) ~~ _om
13 9 12 eqbrtri 
 |-  ( ZZ \ NN ) ~~ _om
14 enfi 
 |-  ( ( ZZ \ NN ) ~~ _om -> ( ( ZZ \ NN ) e. Fin <-> _om e. Fin ) )
15 13 14 ax-mp 
 |-  ( ( ZZ \ NN ) e. Fin <-> _om e. Fin )
16 4 15 mtbir 
 |-  -. ( ZZ \ NN ) e. Fin
17 disjdifr 
 |-  ( ( ZZ \ NN ) i^i NN ) = (/)
18 3 16 17 eldioph4b 
 |-  ( S e. ( Dioph ` N ) <-> ( N e. NN0 /\ E. b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) S = { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } ) )
19 simpr 
 |-  ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) -> a e. ( NN0 ^m ( 1 ... M ) ) )
20 simp-4r 
 |-  ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) -> F : ( 1 ... N ) --> ( 1 ... M ) )
21 ovex 
 |-  ( 1 ... N ) e. _V
22 21 mapco2 
 |-  ( ( a e. ( NN0 ^m ( 1 ... M ) ) /\ F : ( 1 ... N ) --> ( 1 ... M ) ) -> ( a o. F ) e. ( NN0 ^m ( 1 ... N ) ) )
23 19 20 22 syl2anc 
 |-  ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) -> ( a o. F ) e. ( NN0 ^m ( 1 ... N ) ) )
24 uneq1 
 |-  ( c = ( a o. F ) -> ( c u. d ) = ( ( a o. F ) u. d ) )
25 24 fveqeq2d 
 |-  ( c = ( a o. F ) -> ( ( b ` ( c u. d ) ) = 0 <-> ( b ` ( ( a o. F ) u. d ) ) = 0 ) )
26 25 rexbidv 
 |-  ( c = ( a o. F ) -> ( E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 <-> E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( ( a o. F ) u. d ) ) = 0 ) )
27 26 elrab3 
 |-  ( ( a o. F ) e. ( NN0 ^m ( 1 ... N ) ) -> ( ( a o. F ) e. { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } <-> E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( ( a o. F ) u. d ) ) = 0 ) )
28 23 27 syl 
 |-  ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) -> ( ( a o. F ) e. { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } <-> E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( ( a o. F ) u. d ) ) = 0 ) )
29 simp-5r 
 |-  ( ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> F : ( 1 ... N ) --> ( 1 ... M ) )
30 simplr 
 |-  ( ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> a e. ( NN0 ^m ( 1 ... M ) ) )
31 simpr 
 |-  ( ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> d e. ( NN0 ^m ( ZZ \ NN ) ) )
32 coundi 
 |-  ( ( a u. d ) o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) = ( ( ( a u. d ) o. F ) u. ( ( a u. d ) o. ( _I |` ( ZZ \ NN ) ) ) )
33 coundir 
 |-  ( ( a u. d ) o. F ) = ( ( a o. F ) u. ( d o. F ) )
34 elmapi 
 |-  ( d e. ( NN0 ^m ( ZZ \ NN ) ) -> d : ( ZZ \ NN ) --> NN0 )
35 34 3ad2ant3 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> d : ( ZZ \ NN ) --> NN0 )
36 simp1 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> F : ( 1 ... N ) --> ( 1 ... M ) )
37 incom 
 |-  ( ( ZZ \ NN ) i^i ( 1 ... M ) ) = ( ( 1 ... M ) i^i ( ZZ \ NN ) )
38 fz1ssnn 
 |-  ( 1 ... M ) C_ NN
39 disjdif 
 |-  ( NN i^i ( ZZ \ NN ) ) = (/)
40 ssdisj 
 |-  ( ( ( 1 ... M ) C_ NN /\ ( NN i^i ( ZZ \ NN ) ) = (/) ) -> ( ( 1 ... M ) i^i ( ZZ \ NN ) ) = (/) )
41 38 39 40 mp2an 
 |-  ( ( 1 ... M ) i^i ( ZZ \ NN ) ) = (/)
42 37 41 eqtri 
 |-  ( ( ZZ \ NN ) i^i ( 1 ... M ) ) = (/)
43 42 a1i 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( ( ZZ \ NN ) i^i ( 1 ... M ) ) = (/) )
44 coeq0i 
 |-  ( ( d : ( ZZ \ NN ) --> NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) /\ ( ( ZZ \ NN ) i^i ( 1 ... M ) ) = (/) ) -> ( d o. F ) = (/) )
45 35 36 43 44 syl3anc 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( d o. F ) = (/) )
46 45 uneq2d 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( ( a o. F ) u. ( d o. F ) ) = ( ( a o. F ) u. (/) ) )
47 33 46 syl5eq 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( ( a u. d ) o. F ) = ( ( a o. F ) u. (/) ) )
48 un0 
 |-  ( ( a o. F ) u. (/) ) = ( a o. F )
49 47 48 eqtrdi 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( ( a u. d ) o. F ) = ( a o. F ) )
50 coundir 
 |-  ( ( a u. d ) o. ( _I |` ( ZZ \ NN ) ) ) = ( ( a o. ( _I |` ( ZZ \ NN ) ) ) u. ( d o. ( _I |` ( ZZ \ NN ) ) ) )
51 elmapi 
 |-  ( a e. ( NN0 ^m ( 1 ... M ) ) -> a : ( 1 ... M ) --> NN0 )
52 51 3ad2ant2 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> a : ( 1 ... M ) --> NN0 )
53 f1oi 
 |-  ( _I |` ( ZZ \ NN ) ) : ( ZZ \ NN ) -1-1-onto-> ( ZZ \ NN )
54 f1of 
 |-  ( ( _I |` ( ZZ \ NN ) ) : ( ZZ \ NN ) -1-1-onto-> ( ZZ \ NN ) -> ( _I |` ( ZZ \ NN ) ) : ( ZZ \ NN ) --> ( ZZ \ NN ) )
55 53 54 ax-mp 
 |-  ( _I |` ( ZZ \ NN ) ) : ( ZZ \ NN ) --> ( ZZ \ NN )
56 coeq0i 
 |-  ( ( a : ( 1 ... M ) --> NN0 /\ ( _I |` ( ZZ \ NN ) ) : ( ZZ \ NN ) --> ( ZZ \ NN ) /\ ( ( 1 ... M ) i^i ( ZZ \ NN ) ) = (/) ) -> ( a o. ( _I |` ( ZZ \ NN ) ) ) = (/) )
57 55 41 56 mp3an23 
 |-  ( a : ( 1 ... M ) --> NN0 -> ( a o. ( _I |` ( ZZ \ NN ) ) ) = (/) )
58 52 57 syl 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( a o. ( _I |` ( ZZ \ NN ) ) ) = (/) )
59 coires1 
 |-  ( d o. ( _I |` ( ZZ \ NN ) ) ) = ( d |` ( ZZ \ NN ) )
60 ffn 
 |-  ( d : ( ZZ \ NN ) --> NN0 -> d Fn ( ZZ \ NN ) )
61 fnresdm 
 |-  ( d Fn ( ZZ \ NN ) -> ( d |` ( ZZ \ NN ) ) = d )
62 34 60 61 3syl 
 |-  ( d e. ( NN0 ^m ( ZZ \ NN ) ) -> ( d |` ( ZZ \ NN ) ) = d )
63 59 62 syl5eq 
 |-  ( d e. ( NN0 ^m ( ZZ \ NN ) ) -> ( d o. ( _I |` ( ZZ \ NN ) ) ) = d )
64 63 3ad2ant3 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( d o. ( _I |` ( ZZ \ NN ) ) ) = d )
65 58 64 uneq12d 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( ( a o. ( _I |` ( ZZ \ NN ) ) ) u. ( d o. ( _I |` ( ZZ \ NN ) ) ) ) = ( (/) u. d ) )
66 50 65 syl5eq 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( ( a u. d ) o. ( _I |` ( ZZ \ NN ) ) ) = ( (/) u. d ) )
67 uncom 
 |-  ( (/) u. d ) = ( d u. (/) )
68 un0 
 |-  ( d u. (/) ) = d
69 67 68 eqtri 
 |-  ( (/) u. d ) = d
70 66 69 eqtrdi 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( ( a u. d ) o. ( _I |` ( ZZ \ NN ) ) ) = d )
71 49 70 uneq12d 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( ( ( a u. d ) o. F ) u. ( ( a u. d ) o. ( _I |` ( ZZ \ NN ) ) ) ) = ( ( a o. F ) u. d ) )
72 32 71 eqtr2id 
 |-  ( ( F : ( 1 ... N ) --> ( 1 ... M ) /\ a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( ( a o. F ) u. d ) = ( ( a u. d ) o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) )
73 29 30 31 72 syl3anc 
 |-  ( ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( ( a o. F ) u. d ) = ( ( a u. d ) o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) )
74 73 fveq2d 
 |-  ( ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( b ` ( ( a o. F ) u. d ) ) = ( b ` ( ( a u. d ) o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) )
75 nn0ssz 
 |-  NN0 C_ ZZ
76 mapss 
 |-  ( ( ZZ e. _V /\ NN0 C_ ZZ ) -> ( NN0 ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) C_ ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) )
77 1 75 76 mp2an 
 |-  ( NN0 ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) C_ ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) )
78 41 reseq2i 
 |-  ( a |` ( ( 1 ... M ) i^i ( ZZ \ NN ) ) ) = ( a |` (/) )
79 res0 
 |-  ( a |` (/) ) = (/)
80 78 79 eqtri 
 |-  ( a |` ( ( 1 ... M ) i^i ( ZZ \ NN ) ) ) = (/)
81 41 reseq2i 
 |-  ( d |` ( ( 1 ... M ) i^i ( ZZ \ NN ) ) ) = ( d |` (/) )
82 res0 
 |-  ( d |` (/) ) = (/)
83 81 82 eqtri 
 |-  ( d |` ( ( 1 ... M ) i^i ( ZZ \ NN ) ) ) = (/)
84 80 83 eqtr4i 
 |-  ( a |` ( ( 1 ... M ) i^i ( ZZ \ NN ) ) ) = ( d |` ( ( 1 ... M ) i^i ( ZZ \ NN ) ) )
85 elmapresaun 
 |-  ( ( a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) /\ ( a |` ( ( 1 ... M ) i^i ( ZZ \ NN ) ) ) = ( d |` ( ( 1 ... M ) i^i ( ZZ \ NN ) ) ) ) -> ( a u. d ) e. ( NN0 ^m ( ( 1 ... M ) u. ( ZZ \ NN ) ) ) )
86 uncom 
 |-  ( ( 1 ... M ) u. ( ZZ \ NN ) ) = ( ( ZZ \ NN ) u. ( 1 ... M ) )
87 86 oveq2i 
 |-  ( NN0 ^m ( ( 1 ... M ) u. ( ZZ \ NN ) ) ) = ( NN0 ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) )
88 85 87 eleqtrdi 
 |-  ( ( a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) /\ ( a |` ( ( 1 ... M ) i^i ( ZZ \ NN ) ) ) = ( d |` ( ( 1 ... M ) i^i ( ZZ \ NN ) ) ) ) -> ( a u. d ) e. ( NN0 ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) )
89 84 88 mp3an3 
 |-  ( ( a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( a u. d ) e. ( NN0 ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) )
90 77 89 sselid 
 |-  ( ( a e. ( NN0 ^m ( 1 ... M ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( a u. d ) e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) )
91 90 adantll 
 |-  ( ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( a u. d ) e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) )
92 coeq1 
 |-  ( e = ( a u. d ) -> ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) = ( ( a u. d ) o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) )
93 92 fveq2d 
 |-  ( e = ( a u. d ) -> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) = ( b ` ( ( a u. d ) o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) )
94 eqid 
 |-  ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) ) = ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) )
95 fvex 
 |-  ( b ` ( ( a u. d ) o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) e. _V
96 93 94 95 fvmpt 
 |-  ( ( a u. d ) e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) -> ( ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) ) ` ( a u. d ) ) = ( b ` ( ( a u. d ) o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) )
97 91 96 syl 
 |-  ( ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) ) ` ( a u. d ) ) = ( b ` ( ( a u. d ) o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) )
98 74 97 eqtr4d 
 |-  ( ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( b ` ( ( a o. F ) u. d ) ) = ( ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) ) ` ( a u. d ) ) )
99 98 eqeq1d 
 |-  ( ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) /\ d e. ( NN0 ^m ( ZZ \ NN ) ) ) -> ( ( b ` ( ( a o. F ) u. d ) ) = 0 <-> ( ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) ) ` ( a u. d ) ) = 0 ) )
100 99 rexbidva 
 |-  ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) -> ( E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( ( a o. F ) u. d ) ) = 0 <-> E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) ) ` ( a u. d ) ) = 0 ) )
101 28 100 bitrd 
 |-  ( ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) /\ a e. ( NN0 ^m ( 1 ... M ) ) ) -> ( ( a o. F ) e. { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } <-> E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) ) ` ( a u. d ) ) = 0 ) )
102 101 rabbidva 
 |-  ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } } = { a e. ( NN0 ^m ( 1 ... M ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) ) ` ( a u. d ) ) = 0 } )
103 simplll 
 |-  ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) -> M e. NN0 )
104 ovex 
 |-  ( 1 ... M ) e. _V
105 3 104 unex 
 |-  ( ( ZZ \ NN ) u. ( 1 ... M ) ) e. _V
106 105 a1i 
 |-  ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) -> ( ( ZZ \ NN ) u. ( 1 ... M ) ) e. _V )
107 simpr 
 |-  ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) -> b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) )
108 55 a1i 
 |-  ( F : ( 1 ... N ) --> ( 1 ... M ) -> ( _I |` ( ZZ \ NN ) ) : ( ZZ \ NN ) --> ( ZZ \ NN ) )
109 id 
 |-  ( F : ( 1 ... N ) --> ( 1 ... M ) -> F : ( 1 ... N ) --> ( 1 ... M ) )
110 incom 
 |-  ( ( ZZ \ NN ) i^i ( 1 ... N ) ) = ( ( 1 ... N ) i^i ( ZZ \ NN ) )
111 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
112 ssdisj 
 |-  ( ( ( 1 ... N ) C_ NN /\ ( NN i^i ( ZZ \ NN ) ) = (/) ) -> ( ( 1 ... N ) i^i ( ZZ \ NN ) ) = (/) )
113 111 39 112 mp2an 
 |-  ( ( 1 ... N ) i^i ( ZZ \ NN ) ) = (/)
114 110 113 eqtri 
 |-  ( ( ZZ \ NN ) i^i ( 1 ... N ) ) = (/)
115 114 a1i 
 |-  ( F : ( 1 ... N ) --> ( 1 ... M ) -> ( ( ZZ \ NN ) i^i ( 1 ... N ) ) = (/) )
116 fun 
 |-  ( ( ( ( _I |` ( ZZ \ NN ) ) : ( ZZ \ NN ) --> ( ZZ \ NN ) /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ ( ( ZZ \ NN ) i^i ( 1 ... N ) ) = (/) ) -> ( ( _I |` ( ZZ \ NN ) ) u. F ) : ( ( ZZ \ NN ) u. ( 1 ... N ) ) --> ( ( ZZ \ NN ) u. ( 1 ... M ) ) )
117 108 109 115 116 syl21anc 
 |-  ( F : ( 1 ... N ) --> ( 1 ... M ) -> ( ( _I |` ( ZZ \ NN ) ) u. F ) : ( ( ZZ \ NN ) u. ( 1 ... N ) ) --> ( ( ZZ \ NN ) u. ( 1 ... M ) ) )
118 uncom 
 |-  ( ( _I |` ( ZZ \ NN ) ) u. F ) = ( F u. ( _I |` ( ZZ \ NN ) ) )
119 118 feq1i 
 |-  ( ( ( _I |` ( ZZ \ NN ) ) u. F ) : ( ( ZZ \ NN ) u. ( 1 ... N ) ) --> ( ( ZZ \ NN ) u. ( 1 ... M ) ) <-> ( F u. ( _I |` ( ZZ \ NN ) ) ) : ( ( ZZ \ NN ) u. ( 1 ... N ) ) --> ( ( ZZ \ NN ) u. ( 1 ... M ) ) )
120 117 119 sylib 
 |-  ( F : ( 1 ... N ) --> ( 1 ... M ) -> ( F u. ( _I |` ( ZZ \ NN ) ) ) : ( ( ZZ \ NN ) u. ( 1 ... N ) ) --> ( ( ZZ \ NN ) u. ( 1 ... M ) ) )
121 120 ad3antlr 
 |-  ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) -> ( F u. ( _I |` ( ZZ \ NN ) ) ) : ( ( ZZ \ NN ) u. ( 1 ... N ) ) --> ( ( ZZ \ NN ) u. ( 1 ... M ) ) )
122 mzprename 
 |-  ( ( ( ( ZZ \ NN ) u. ( 1 ... M ) ) e. _V /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) /\ ( F u. ( _I |` ( ZZ \ NN ) ) ) : ( ( ZZ \ NN ) u. ( 1 ... N ) ) --> ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) -> ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) ) e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) )
123 106 107 121 122 syl3anc 
 |-  ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) -> ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) ) e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) )
124 3 16 17 eldioph4i 
 |-  ( ( M e. NN0 /\ ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) ) e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) ) ` ( a u. d ) ) = 0 } e. ( Dioph ` M ) )
125 103 123 124 syl2anc 
 |-  ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( ( e e. ( ZZ ^m ( ( ZZ \ NN ) u. ( 1 ... M ) ) ) |-> ( b ` ( e o. ( F u. ( _I |` ( ZZ \ NN ) ) ) ) ) ) ` ( a u. d ) ) = 0 } e. ( Dioph ` M ) )
126 102 125 eqeltrd 
 |-  ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } } e. ( Dioph ` M ) )
127 eleq2 
 |-  ( S = { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } -> ( ( a o. F ) e. S <-> ( a o. F ) e. { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } ) )
128 127 rabbidv 
 |-  ( S = { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } -> { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. S } = { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } } )
129 128 eleq1d 
 |-  ( S = { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } -> ( { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. S } e. ( Dioph ` M ) <-> { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } } e. ( Dioph ` M ) ) )
130 126 129 syl5ibrcom 
 |-  ( ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) /\ b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) ) -> ( S = { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } -> { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. S } e. ( Dioph ` M ) ) )
131 130 rexlimdva 
 |-  ( ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) /\ N e. NN0 ) -> ( E. b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) S = { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } -> { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. S } e. ( Dioph ` M ) ) )
132 131 expimpd 
 |-  ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) -> ( ( N e. NN0 /\ E. b e. ( mzPoly ` ( ( ZZ \ NN ) u. ( 1 ... N ) ) ) S = { c e. ( NN0 ^m ( 1 ... N ) ) | E. d e. ( NN0 ^m ( ZZ \ NN ) ) ( b ` ( c u. d ) ) = 0 } ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. S } e. ( Dioph ` M ) ) )
133 18 132 syl5bi 
 |-  ( ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) -> ( S e. ( Dioph ` N ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. S } e. ( Dioph ` M ) ) )
134 133 impcom 
 |-  ( ( S e. ( Dioph ` N ) /\ ( M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. S } e. ( Dioph ` M ) )
135 134 3impb 
 |-  ( ( S e. ( Dioph ` N ) /\ M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. S } e. ( Dioph ` M ) )