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 fcdmnn0supp 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 94 69 95 96 4syl f 0 J R bits 0 f = bits f
98 97 mpteq2ia f 0 J R bits 0 f = f 0 J R bits f
99 98 eqcomi f 0 J R bits f = f 0 J R bits 0 f
100 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
101 99 100 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
102 93 101 mpbird f 0 J R bits f : 0 J R 1-1 onto r 𝒫 0 Fin J | r supp Fin
103 102 mptru f 0 J R bits f : 0 J R 1-1 onto r 𝒫 0 Fin J | r supp Fin
104 ssrab2 z | ¬ 2 z
105 4 104 eqsstri J
106 11 58 105 3pm3.2i V 0 V J
107 cnveq f = o f -1 = o -1
108 dfn2 = 0 0
109 108 a1i f = o = 0 0
110 107 109 imaeq12d f = o f -1 = o -1 0 0
111 110 sseq1d f = o f -1 J o -1 0 0 J
112 111 cbvrabv f 0 | f -1 J = o 0 | o -1 0 0 J
113 9 112 eqtri T = o 0 | o -1 0 0 J
114 eqid o T o J = o T o J
115 113 114 resf1o V 0 V J 0 0 o T o J : T 1-1 onto 0 J
116 106 63 115 mp2an o T o J : T 1-1 onto 0 J
117 f1of1 o T o J : T 1-1 onto 0 J o T o J : T 1-1 0 J
118 116 117 ax-mp o T o J : T 1-1 0 J
119 inss1 T R T
120 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
121 118 119 120 mp2an o T o J T R : T R 1-1 onto o T o J T R
122 vex o V
123 122 resex o J V
124 123 114 fnmpti o T o J Fn T
125 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
126 124 119 125 mp2an f o T o J T R m T R o T o J m = f
127 eqid m T R m J = m T R m J
128 vex m V
129 128 resex m J V
130 127 129 elrnmpti f ran m T R m J m T R f = m J
131 1 2 3 4 5 6 7 8 9 eulerpartlemt 0 J R = ran m T R m J
132 131 eleq2i f 0 J R f ran m T R m J
133 elinel1 m T R m T
134 114 fvtresfn m T o T o J m = m J
135 134 eqeq1d m T o T o J m = f m J = f
136 133 135 syl m T R o T o J m = f m J = f
137 eqcom m J = f f = m J
138 136 137 bitrdi m T R o T o J m = f f = m J
139 138 rexbiia m T R o T o J m = f m T R f = m J
140 130 132 139 3bitr4ri m T R o T o J m = f f 0 J R
141 126 140 bitri f o T o J T R f 0 J R
142 141 eqriv o T o J T R = 0 J R
143 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
144 142 143 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
145 resmpt T R T o T o J T R = o T R o J
146 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
147 119 145 146 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
148 144 147 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
149 121 148 mpbi o T R o J : T R 1-1 onto 0 J R
150 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
151 103 149 150 mp2an f 0 J R bits f o T R o J : T R 1-1 onto r 𝒫 0 Fin J | r supp Fin
152 f1of o T R o J : T R 1-1 onto 0 J R o T R o J : T R 0 J R
153 eqid o T R o J = o T R o J
154 153 fmpt o T R o J 0 J R o T R o J : T R 0 J R
155 154 biimpri o T R o J : T R 0 J R o T R o J 0 J R
156 149 152 155 mp2b o T R o J 0 J R
157 156 a1i o T R o J 0 J R
158 eqidd o T R o J = o T R o J
159 eqidd f 0 J R bits f = f 0 J R bits f
160 coeq2 f = o J bits f = bits o J
161 157 158 159 160 fmptcof f 0 J R bits f o T R o J = o T R bits o J
162 161 eqcomd o T R bits o J = f 0 J R bits f o T R o J
163 eqidd T R = T R
164 6 a1i H = r 𝒫 0 Fin J | r supp Fin
165 162 163 164 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
166 151 165 mpbiri o T R bits o J : T R 1-1 onto H
167 166 mptru o T R bits o J : T R 1-1 onto H
168 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
169 53 167 168 mp2an M o T R bits o J : T R 1-1 onto 𝒫 J × 0 Fin
170 eqidd o T R bits o J = o T R bits o J
171 bitsf bits : 𝒫 0
172 zex V
173 fex bits : 𝒫 0 V bits V
174 171 172 173 mp2an bits V
175 174 123 coex bits o J V
176 175 a1i o T R bits o J V
177 170 176 fvmpt2d o T R o T R bits o J o = bits o J
178 f1of o T R bits o J : T R 1-1 onto H o T R bits o J : T R H
179 166 178 syl o T R bits o J : T R H
180 179 ffvelcdmda o T R o T R bits o J o H
181 177 180 eqeltrrd o T R bits o J H
182 f1ofn M : H 1-1 onto 𝒫 J × 0 Fin M Fn H
183 53 182 ax-mp M Fn H
184 dffn5 M Fn H M = r H M r
185 183 184 mpbi M = r H M r
186 185 a1i M = r H M r
187 fveq2 r = bits o J M r = M bits o J
188 181 170 186 187 fmptco M o T R bits o J = o T R M bits o J
189 188 mptru M o T R bits o J = o T R M bits o J
190 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
191 189 190 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
192 169 191 mpbi o T R M bits o J : T R 1-1 onto 𝒫 J × 0 Fin
193 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
194 52 192 193 mp2an a 𝒫 J × 0 Fin F a o T R M bits o J : T R 1-1 onto 𝒫 Fin
195 simpr o T R o T R
196 fvex M bits o J V
197 eqid o T R M bits o J = o T R M bits o J
198 197 fvmpt2 o T R M bits o J V o T R M bits o J o = M bits o J
199 195 196 198 sylancl o T R o T R M bits o J o = M bits o J
200 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
201 192 200 mp1i o T R M bits o J : T R 𝒫 J × 0 Fin
202 201 ffvelcdmda o T R o T R M bits o J o 𝒫 J × 0 Fin
203 199 202 eqeltrrd o T R M bits o J 𝒫 J × 0 Fin
204 eqidd o T R M bits o J = o T R M bits o J
205 eqidd a 𝒫 J × 0 Fin F a = a 𝒫 J × 0 Fin F a
206 imaeq2 a = M bits o J F a = F M bits o J
207 203 204 205 206 fmptco a 𝒫 J × 0 Fin F a o T R M bits o J = o T R F M bits o J
208 207 mptru a 𝒫 J × 0 Fin F a o T R M bits o J = o T R F M bits o J
209 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
210 208 209 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
211 194 210 mpbi o T R F M bits o J : T R 1-1 onto 𝒫 Fin
212 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
213 49 211 212 mp2an 𝟙 Fin o T R F M bits o J : T R 1-1 onto 0 1 R
214 5 mpoexg J V 0 V F V
215 56 58 214 mp2an F V
216 imaexg F V F M bits o J V
217 215 216 ax-mp F M bits o J V
218 eqid o T R F M bits o J = o T R F M bits o J
219 218 fvmpt2 o T R F M bits o J V o T R F M bits o J o = F M bits o J
220 195 217 219 sylancl o T R o T R F M bits o J o = F M bits o J
221 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
222 211 221 mp1i o T R F M bits o J : T R 𝒫 Fin
223 222 ffvelcdmda o T R o T R F M bits o J o 𝒫 Fin
224 220 223 eqeltrrd o T R F M bits o J 𝒫 Fin
225 eqidd o T R F M bits o J = o T R F M bits o J
226 indf1o V 𝟙 : 𝒫 1-1 onto 0 1
227 f1ofn 𝟙 : 𝒫 1-1 onto 0 1 𝟙 Fn 𝒫
228 11 226 227 mp2b 𝟙 Fn 𝒫
229 dffn5 𝟙 Fn 𝒫 𝟙 = b 𝒫 𝟙 b
230 228 229 mpbi 𝟙 = b 𝒫 𝟙 b
231 230 reseq1i 𝟙 Fin = b 𝒫 𝟙 b Fin
232 resmpt3 b 𝒫 𝟙 b Fin = b 𝒫 Fin 𝟙 b
233 231 232 eqtri 𝟙 Fin = b 𝒫 Fin 𝟙 b
234 233 a1i 𝟙 Fin = b 𝒫 Fin 𝟙 b
235 fveq2 b = F M bits o J 𝟙 b = 𝟙 F M bits o J
236 224 225 234 235 fmptco 𝟙 Fin o T R F M bits o J = o T R 𝟙 F M bits o J
237 236 mptru 𝟙 Fin o T R F M bits o J = o T R 𝟙 F M bits o J
238 10 237 eqtr4i G = 𝟙 Fin o T R F M bits o J
239 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
240 238 239 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
241 213 240 mpbir G : T R 1-1 onto 0 1 R