Metamath Proof Explorer


Theorem eulerpartgbij

Description: Lemma for eulerpart : The G function is a bijection. (Contributed by Thierry Arnoux, 27-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses eulerpart.p P = f 0 | f -1 Fin k f k k = N
eulerpart.o O = g P | n g -1 ¬ 2 n
eulerpart.d D = g P | n g n 1
eulerpart.j J = z | ¬ 2 z
eulerpart.f F = x J , y 0 2 y x
eulerpart.h H = r 𝒫 0 Fin J | r supp Fin
eulerpart.m M = r H x y | x J y r x
eulerpart.r R = f | f -1 Fin
eulerpart.t T = f 0 | f -1 J
eulerpart.g G = o T R 𝟙 F M bits o J
Assertion eulerpartgbij G : T R 1-1 onto 0 1 R

Proof

Step Hyp Ref Expression
1 eulerpart.p P = f 0 | f -1 Fin k f k k = N
2 eulerpart.o O = g P | n g -1 ¬ 2 n
3 eulerpart.d D = g P | n g n 1
4 eulerpart.j J = z | ¬ 2 z
5 eulerpart.f F = x J , y 0 2 y x
6 eulerpart.h H = r 𝒫 0 Fin J | r supp Fin
7 eulerpart.m M = r H x y | x J y r x
8 eulerpart.r R = f | f -1 Fin
9 eulerpart.t T = f 0 | f -1 J
10 eulerpart.g G = o T R 𝟙 F M bits o J
11 nnex V
12 indf1ofs V 𝟙 Fin : 𝒫 Fin 1-1 onto f 0 1 | f -1 1 Fin
13 11 12 ax-mp 𝟙 Fin : 𝒫 Fin 1-1 onto f 0 1 | f -1 1 Fin
14 incom 0 1 f | f -1 Fin = f | f -1 Fin 0 1
15 8 ineq2i 0 1 R = 0 1 f | f -1 Fin
16 dfrab2 f 0 1 | f -1 Fin = f | f -1 Fin 0 1
17 14 15 16 3eqtr4i 0 1 R = f 0 1 | f -1 Fin
18 elmapfun f 0 1 Fun f
19 elmapi f 0 1 f : 0 1
20 19 frnd f 0 1 ran f 0 1
21 fimacnvinrn2 Fun f ran f 0 1 f -1 = f -1 0 1
22 df-pr 0 1 = 0 1
23 22 ineq2i 0 1 = 0 1
24 indi 0 1 = 0 1
25 0nnn ¬ 0
26 disjsn 0 = ¬ 0
27 25 26 mpbir 0 =
28 1nn 1
29 1ex 1 V
30 29 snss 1 1
31 28 30 mpbi 1
32 dfss 1 1 = 1
33 31 32 mpbi 1 = 1
34 incom 1 = 1
35 33 34 eqtr2i 1 = 1
36 27 35 uneq12i 0 1 = 1
37 23 24 36 3eqtri 0 1 = 1
38 uncom 1 = 1
39 un0 1 = 1
40 37 38 39 3eqtri 0 1 = 1
41 40 imaeq2i f -1 0 1 = f -1 1
42 21 41 eqtrdi Fun f ran f 0 1 f -1 = f -1 1
43 18 20 42 syl2anc f 0 1 f -1 = f -1 1
44 43 eleq1d f 0 1 f -1 Fin f -1 1 Fin
45 44 rabbiia f 0 1 | f -1 Fin = f 0 1 | f -1 1 Fin
46 17 45 eqtr2i f 0 1 | f -1 1 Fin = 0 1 R
47 f1oeq3 f 0 1 | f -1 1 Fin = 0 1 R 𝟙 Fin : 𝒫 Fin 1-1 onto f 0 1 | f -1 1 Fin 𝟙 Fin : 𝒫 Fin 1-1 onto 0 1 R
48 46 47 ax-mp 𝟙 Fin : 𝒫 Fin 1-1 onto f 0 1 | f -1 1 Fin 𝟙 Fin : 𝒫 Fin 1-1 onto 0 1 R
49 13 48 mpbi 𝟙 Fin : 𝒫 Fin 1-1 onto 0 1 R
50 4 5 oddpwdc F : J × 0 1-1 onto
51 f1opwfi F : J × 0 1-1 onto a 𝒫 J × 0 Fin F a : 𝒫 J × 0 Fin 1-1 onto 𝒫 Fin
52 50 51 ax-mp a 𝒫 J × 0 Fin F a : 𝒫 J × 0 Fin 1-1 onto 𝒫 Fin
53 1 2 3 4 5 6 7 eulerpartlem1 M : H 1-1 onto 𝒫 J × 0 Fin
54 bitsf1o bits 0 : 0 1-1 onto 𝒫 0 Fin
55 54 a1i bits 0 : 0 1-1 onto 𝒫 0 Fin
56 4 11 rabex2 J V
57 56 a1i J V
58 nn0ex 0 V
59 58 a1i 0 V
60 58 pwex 𝒫 0 V
61 60 inex1 𝒫 0 Fin V
62 61 a1i 𝒫 0 Fin V
63 0nn0 0 0
64 63 a1i 0 0
65 fvres 0 0 bits 0 0 = bits 0
66 63 65 ax-mp bits 0 0 = bits 0
67 0bits bits 0 =
68 66 67 eqtr2i = bits 0 0
69 elmapi f 0 J f : J 0
70 frnnn0supp J V f : J 0 f supp 0 = f -1
71 56 69 70 sylancr f 0 J f supp 0 = f -1
72 71 eleq1d f 0 J f supp 0 Fin f -1 Fin
73 72 rabbiia f 0 J | f supp 0 Fin = f 0 J | f -1 Fin
74 elmapfun f 0 J Fun f
75 vex f V
76 funisfsupp Fun f f V 0 0 finSupp 0 f f supp 0 Fin
77 75 63 76 mp3an23 Fun f finSupp 0 f f supp 0 Fin
78 74 77 syl f 0 J finSupp 0 f f supp 0 Fin
79 78 rabbiia f 0 J | finSupp 0 f = f 0 J | f supp 0 Fin
80 incom f | f -1 Fin 0 J = 0 J f | f -1 Fin
81 dfrab2 f 0 J | f -1 Fin = f | f -1 Fin 0 J
82 8 ineq2i 0 J R = 0 J f | f -1 Fin
83 80 81 82 3eqtr4ri 0 J R = f 0 J | f -1 Fin
84 73 79 83 3eqtr4ri 0 J R = f 0 J | finSupp 0 f
85 elmapfun r 𝒫 0 Fin J Fun r
86 vex r V
87 0ex V
88 funisfsupp Fun r r V V finSupp r r supp Fin
89 86 87 88 mp3an23 Fun r finSupp r r supp Fin
90 89 bicomd Fun r r supp Fin finSupp r
91 85 90 syl r 𝒫 0 Fin J r supp Fin finSupp r
92 91 rabbiia r 𝒫 0 Fin J | r supp Fin = r 𝒫 0 Fin J | finSupp r
93 55 57 59 62 64 68 84 92 fcobijfs f 0 J R bits 0 f : 0 J R 1-1 onto r 𝒫 0 Fin J | r supp Fin
94 elinel1 f 0 J R f 0 J
95 frn f : J 0 ran f 0
96 cores ran f 0 bits 0 f = bits f
97 69 95 96 3syl f 0 J bits 0 f = bits f
98 94 97 syl f 0 J R bits 0 f = bits f
99 98 mpteq2ia f 0 J R bits 0 f = f 0 J R bits f
100 99 eqcomi f 0 J R bits f = f 0 J R bits 0 f
101 f1oeq1 f 0 J R bits f = f 0 J R bits 0 f f 0 J R bits f : 0 J R 1-1 onto r 𝒫 0 Fin J | r supp Fin f 0 J R bits 0 f : 0 J R 1-1 onto r 𝒫 0 Fin J | r supp Fin
102 100 101 mp1i f 0 J R bits f : 0 J R 1-1 onto r 𝒫 0 Fin J | r supp Fin f 0 J R bits 0 f : 0 J R 1-1 onto r 𝒫 0 Fin J | r supp Fin
103 93 102 mpbird f 0 J R bits f : 0 J R 1-1 onto r 𝒫 0 Fin J | r supp Fin
104 103 mptru f 0 J R bits f : 0 J R 1-1 onto r 𝒫 0 Fin J | r supp Fin
105 ssrab2 z | ¬ 2 z
106 4 105 eqsstri J
107 11 58 106 3pm3.2i V 0 V J
108 cnveq f = o f -1 = o -1
109 dfn2 = 0 0
110 109 a1i f = o = 0 0
111 108 110 imaeq12d f = o f -1 = o -1 0 0
112 111 sseq1d f = o f -1 J o -1 0 0 J
113 112 cbvrabv f 0 | f -1 J = o 0 | o -1 0 0 J
114 9 113 eqtri T = o 0 | o -1 0 0 J
115 eqid o T o J = o T o J
116 114 115 resf1o V 0 V J 0 0 o T o J : T 1-1 onto 0 J
117 107 63 116 mp2an o T o J : T 1-1 onto 0 J
118 f1of1 o T o J : T 1-1 onto 0 J o T o J : T 1-1 0 J
119 117 118 ax-mp o T o J : T 1-1 0 J
120 inss1 T R T
121 f1ores o T o J : T 1-1 0 J T R T o T o J T R : T R 1-1 onto o T o J T R
122 119 120 121 mp2an o T o J T R : T R 1-1 onto o T o J T R
123 vex o V
124 123 resex o J V
125 124 115 fnmpti o T o J Fn T
126 fvelimab o T o J Fn T T R T f o T o J T R m T R o T o J m = f
127 125 120 126 mp2an f o T o J T R m T R o T o J m = f
128 eqid m T R m J = m T R m J
129 vex m V
130 129 resex m J V
131 128 130 elrnmpti f ran m T R m J m T R f = m J
132 1 2 3 4 5 6 7 8 9 eulerpartlemt 0 J R = ran m T R m J
133 132 eleq2i f 0 J R f ran m T R m J
134 elinel1 m T R m T
135 115 fvtresfn m T o T o J m = m J
136 135 eqeq1d m T o T o J m = f m J = f
137 134 136 syl m T R o T o J m = f m J = f
138 eqcom m J = f f = m J
139 137 138 bitrdi m T R o T o J m = f f = m J
140 139 rexbiia m T R o T o J m = f m T R f = m J
141 131 133 140 3bitr4ri m T R o T o J m = f f 0 J R
142 127 141 bitri f o T o J T R f 0 J R
143 142 eqriv o T o J T R = 0 J R
144 f1oeq3 o T o J T R = 0 J R o T o J T R : T R 1-1 onto o T o J T R o T o J T R : T R 1-1 onto 0 J R
145 143 144 ax-mp o T o J T R : T R 1-1 onto o T o J T R o T o J T R : T R 1-1 onto 0 J R
146 resmpt T R T o T o J T R = o T R o J
147 f1oeq1 o T o J T R = o T R o J o T o J T R : T R 1-1 onto 0 J R o T R o J : T R 1-1 onto 0 J R
148 120 146 147 mp2b o T o J T R : T R 1-1 onto 0 J R o T R o J : T R 1-1 onto 0 J R
149 145 148 bitri o T o J T R : T R 1-1 onto o T o J T R o T R o J : T R 1-1 onto 0 J R
150 122 149 mpbi o T R o J : T R 1-1 onto 0 J R
151 f1oco f 0 J R bits f : 0 J R 1-1 onto r 𝒫 0 Fin J | r supp Fin o T R o J : T R 1-1 onto 0 J R f 0 J R bits f o T R o J : T R 1-1 onto r 𝒫 0 Fin J | r supp Fin
152 104 150 151 mp2an f 0 J R bits f o T R o J : T R 1-1 onto r 𝒫 0 Fin J | r supp Fin
153 f1of o T R o J : T R 1-1 onto 0 J R o T R o J : T R 0 J R
154 eqid o T R o J = o T R o J
155 154 fmpt o T R o J 0 J R o T R o J : T R 0 J R
156 155 biimpri o T R o J : T R 0 J R o T R o J 0 J R
157 150 153 156 mp2b o T R o J 0 J R
158 157 a1i o T R o J 0 J R
159 eqidd o T R o J = o T R o J
160 eqidd f 0 J R bits f = f 0 J R bits f
161 coeq2 f = o J bits f = bits o J
162 158 159 160 161 fmptcof f 0 J R bits f o T R o J = o T R bits o J
163 162 eqcomd o T R bits o J = f 0 J R bits f o T R o J
164 eqidd T R = T R
165 6 a1i H = r 𝒫 0 Fin J | r supp Fin
166 163 164 165 f1oeq123d o T R bits o J : T R 1-1 onto H f 0 J R bits f o T R o J : T R 1-1 onto r 𝒫 0 Fin J | r supp Fin
167 152 166 mpbiri o T R bits o J : T R 1-1 onto H
168 167 mptru o T R bits o J : T R 1-1 onto H
169 f1oco M : H 1-1 onto 𝒫 J × 0 Fin o T R bits o J : T R 1-1 onto H M o T R bits o J : T R 1-1 onto 𝒫 J × 0 Fin
170 53 168 169 mp2an M o T R bits o J : T R 1-1 onto 𝒫 J × 0 Fin
171 eqidd o T R bits o J = o T R bits o J
172 bitsf bits : 𝒫 0
173 zex V
174 fex bits : 𝒫 0 V bits V
175 172 173 174 mp2an bits V
176 175 124 coex bits o J V
177 176 a1i o T R bits o J V
178 171 177 fvmpt2d o T R o T R bits o J o = bits o J
179 f1of o T R bits o J : T R 1-1 onto H o T R bits o J : T R H
180 167 179 syl o T R bits o J : T R H
181 180 ffvelrnda o T R o T R bits o J o H
182 178 181 eqeltrrd o T R bits o J H
183 f1ofn M : H 1-1 onto 𝒫 J × 0 Fin M Fn H
184 53 183 ax-mp M Fn H
185 dffn5 M Fn H M = r H M r
186 184 185 mpbi M = r H M r
187 186 a1i M = r H M r
188 fveq2 r = bits o J M r = M bits o J
189 182 171 187 188 fmptco M o T R bits o J = o T R M bits o J
190 189 mptru M o T R bits o J = o T R M bits o J
191 f1oeq1 M o T R bits o J = o T R M bits o J M o T R bits o J : T R 1-1 onto 𝒫 J × 0 Fin o T R M bits o J : T R 1-1 onto 𝒫 J × 0 Fin
192 190 191 ax-mp M o T R bits o J : T R 1-1 onto 𝒫 J × 0 Fin o T R M bits o J : T R 1-1 onto 𝒫 J × 0 Fin
193 170 192 mpbi o T R M bits o J : T R 1-1 onto 𝒫 J × 0 Fin
194 f1oco a 𝒫 J × 0 Fin F a : 𝒫 J × 0 Fin 1-1 onto 𝒫 Fin o T R M bits o J : T R 1-1 onto 𝒫 J × 0 Fin a 𝒫 J × 0 Fin F a o T R M bits o J : T R 1-1 onto 𝒫 Fin
195 52 193 194 mp2an a 𝒫 J × 0 Fin F a o T R M bits o J : T R 1-1 onto 𝒫 Fin
196 simpr o T R o T R
197 fvex M bits o J V
198 eqid o T R M bits o J = o T R M bits o J
199 198 fvmpt2 o T R M bits o J V o T R M bits o J o = M bits o J
200 196 197 199 sylancl o T R o T R M bits o J o = M bits o J
201 f1of o T R M bits o J : T R 1-1 onto 𝒫 J × 0 Fin o T R M bits o J : T R 𝒫 J × 0 Fin
202 193 201 mp1i o T R M bits o J : T R 𝒫 J × 0 Fin
203 202 ffvelrnda o T R o T R M bits o J o 𝒫 J × 0 Fin
204 200 203 eqeltrrd o T R M bits o J 𝒫 J × 0 Fin
205 eqidd o T R M bits o J = o T R M bits o J
206 eqidd a 𝒫 J × 0 Fin F a = a 𝒫 J × 0 Fin F a
207 imaeq2 a = M bits o J F a = F M bits o J
208 204 205 206 207 fmptco a 𝒫 J × 0 Fin F a o T R M bits o J = o T R F M bits o J
209 208 mptru a 𝒫 J × 0 Fin F a o T R M bits o J = o T R F M bits o J
210 f1oeq1 a 𝒫 J × 0 Fin F a o T R M bits o J = o T R F M bits o J a 𝒫 J × 0 Fin F a o T R M bits o J : T R 1-1 onto 𝒫 Fin o T R F M bits o J : T R 1-1 onto 𝒫 Fin
211 209 210 ax-mp a 𝒫 J × 0 Fin F a o T R M bits o J : T R 1-1 onto 𝒫 Fin o T R F M bits o J : T R 1-1 onto 𝒫 Fin
212 195 211 mpbi o T R F M bits o J : T R 1-1 onto 𝒫 Fin
213 f1oco 𝟙 Fin : 𝒫 Fin 1-1 onto 0 1 R o T R F M bits o J : T R 1-1 onto 𝒫 Fin 𝟙 Fin o T R F M bits o J : T R 1-1 onto 0 1 R
214 49 212 213 mp2an 𝟙 Fin o T R F M bits o J : T R 1-1 onto 0 1 R
215 5 mpoexg J V 0 V F V
216 56 58 215 mp2an F V
217 imaexg F V F M bits o J V
218 216 217 ax-mp F M bits o J V
219 eqid o T R F M bits o J = o T R F M bits o J
220 219 fvmpt2 o T R F M bits o J V o T R F M bits o J o = F M bits o J
221 196 218 220 sylancl o T R o T R F M bits o J o = F M bits o J
222 f1of o T R F M bits o J : T R 1-1 onto 𝒫 Fin o T R F M bits o J : T R 𝒫 Fin
223 212 222 mp1i o T R F M bits o J : T R 𝒫 Fin
224 223 ffvelrnda o T R o T R F M bits o J o 𝒫 Fin
225 221 224 eqeltrrd o T R F M bits o J 𝒫 Fin
226 eqidd o T R F M bits o J = o T R F M bits o J
227 indf1o V 𝟙 : 𝒫 1-1 onto 0 1
228 f1ofn 𝟙 : 𝒫 1-1 onto 0 1 𝟙 Fn 𝒫
229 11 227 228 mp2b 𝟙 Fn 𝒫
230 dffn5 𝟙 Fn 𝒫 𝟙 = b 𝒫 𝟙 b
231 229 230 mpbi 𝟙 = b 𝒫 𝟙 b
232 231 reseq1i 𝟙 Fin = b 𝒫 𝟙 b Fin
233 resmpt3 b 𝒫 𝟙 b Fin = b 𝒫 Fin 𝟙 b
234 232 233 eqtri 𝟙 Fin = b 𝒫 Fin 𝟙 b
235 234 a1i 𝟙 Fin = b 𝒫 Fin 𝟙 b
236 fveq2 b = F M bits o J 𝟙 b = 𝟙 F M bits o J
237 225 226 235 236 fmptco 𝟙 Fin o T R F M bits o J = o T R 𝟙 F M bits o J
238 237 mptru 𝟙 Fin o T R F M bits o J = o T R 𝟙 F M bits o J
239 10 238 eqtr4i G = 𝟙 Fin o T R F M bits o J
240 f1oeq1 G = 𝟙 Fin o T R F M bits o J G : T R 1-1 onto 0 1 R 𝟙 Fin o T R F M bits o J : T R 1-1 onto 0 1 R
241 239 240 ax-mp G : T R 1-1 onto 0 1 R 𝟙 Fin o T R F M bits o J : T R 1-1 onto 0 1 R
242 214 241 mpbir G : T R 1-1 onto 0 1 R