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 Dioph N M 0 F : 1 N 1 M a 0 1 M | a F S Dioph M

Proof

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