Metamath Proof Explorer

Theorem eulerpartlemmf

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 30-Aug-2018) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses eulerpart.p 
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
eulerpart.o 
|- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
eulerpart.d 
|- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
eulerpart.j 
|- J = { z e. NN | -. 2 || z }
eulerpart.f 
|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
eulerpart.h 
|- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
eulerpart.m 
|- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
eulerpart.r 
|- R = { f | ( `' f " NN ) e. Fin }
eulerpart.t 
|- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
eulerpart.g 
|- G = ( o e. ( T i^i R ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
Assertion eulerpartlemmf 
|- ( A e. ( T i^i R ) -> ( bits o. ( A |` J ) ) e. H )

Proof

Step Hyp Ref Expression
1 eulerpart.p 
 |-  P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
2 eulerpart.o 
 |-  O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
3 eulerpart.d 
 |-  D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
4 eulerpart.j 
 |-  J = { z e. NN | -. 2 || z }
5 eulerpart.f 
 |-  F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
6 eulerpart.h 
 |-  H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
7 eulerpart.m 
 |-  M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
8 eulerpart.r 
 |-  R = { f | ( `' f " NN ) e. Fin }
9 eulerpart.t 
 |-  T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
10 eulerpart.g 
 |-  G = ( o e. ( T i^i R ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
11 bitsf1o 
 |-  ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
12 f1of 
 |-  ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) -> ( bits |` NN0 ) : NN0 --> ( ~P NN0 i^i Fin ) )
13 11 12 ax-mp 
 |-  ( bits |` NN0 ) : NN0 --> ( ~P NN0 i^i Fin )
14 1 2 3 4 5 6 7 8 9 eulerpartlemt0 
 |-  ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )
15 14 biimpi 
 |-  ( A e. ( T i^i R ) -> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )
16 15 simp1d 
 |-  ( A e. ( T i^i R ) -> A e. ( NN0 ^m NN ) )
17 nn0ex 
 |-  NN0 e. _V
18 nnex 
 |-  NN e. _V
19 17 18 elmap 
 |-  ( A e. ( NN0 ^m NN ) <-> A : NN --> NN0 )
20 16 19 sylib 
 |-  ( A e. ( T i^i R ) -> A : NN --> NN0 )
21 ssrab2 
 |-  { z e. NN | -. 2 || z } C_ NN
22 4 21 eqsstri 
 |-  J C_ NN
23 fssres 
 |-  ( ( A : NN --> NN0 /\ J C_ NN ) -> ( A |` J ) : J --> NN0 )
24 20 22 23 sylancl 
 |-  ( A e. ( T i^i R ) -> ( A |` J ) : J --> NN0 )
25 fco2 
 |-  ( ( ( bits |` NN0 ) : NN0 --> ( ~P NN0 i^i Fin ) /\ ( A |` J ) : J --> NN0 ) -> ( bits o. ( A |` J ) ) : J --> ( ~P NN0 i^i Fin ) )
26 13 24 25 sylancr 
 |-  ( A e. ( T i^i R ) -> ( bits o. ( A |` J ) ) : J --> ( ~P NN0 i^i Fin ) )
27 17 pwex 
 |-  ~P NN0 e. _V
28 27 inex1 
 |-  ( ~P NN0 i^i Fin ) e. _V
29 18 22 ssexi 
 |-  J e. _V
30 28 29 elmap 
 |-  ( ( bits o. ( A |` J ) ) e. ( ( ~P NN0 i^i Fin ) ^m J ) <-> ( bits o. ( A |` J ) ) : J --> ( ~P NN0 i^i Fin ) )
31 26 30 sylibr 
 |-  ( A e. ( T i^i R ) -> ( bits o. ( A |` J ) ) e. ( ( ~P NN0 i^i Fin ) ^m J ) )
32 15 simp2d 
 |-  ( A e. ( T i^i R ) -> ( `' A " NN ) e. Fin )
33 0nn0 
 |-  0 e. NN0
34 suppimacnv 
 |-  ( ( A e. ( T i^i R ) /\ 0 e. NN0 ) -> ( A supp 0 ) = ( `' A " ( _V \ { 0 } ) ) )
35 33 34 mpan2 
 |-  ( A e. ( T i^i R ) -> ( A supp 0 ) = ( `' A " ( _V \ { 0 } ) ) )
36 frnsuppeq 
 |-  ( ( NN e. _V /\ 0 e. NN0 ) -> ( A : NN --> NN0 -> ( A supp 0 ) = ( `' A " ( NN0 \ { 0 } ) ) ) )
37 18 33 36 mp2an 
 |-  ( A : NN --> NN0 -> ( A supp 0 ) = ( `' A " ( NN0 \ { 0 } ) ) )
38 20 37 syl 
 |-  ( A e. ( T i^i R ) -> ( A supp 0 ) = ( `' A " ( NN0 \ { 0 } ) ) )
39 35 38 eqtr3d 
 |-  ( A e. ( T i^i R ) -> ( `' A " ( _V \ { 0 } ) ) = ( `' A " ( NN0 \ { 0 } ) ) )
40 39 eleq1d 
 |-  ( A e. ( T i^i R ) -> ( ( `' A " ( _V \ { 0 } ) ) e. Fin <-> ( `' A " ( NN0 \ { 0 } ) ) e. Fin ) )
41 dfn2 
 |-  NN = ( NN0 \ { 0 } )
42 41 imaeq2i 
 |-  ( `' A " NN ) = ( `' A " ( NN0 \ { 0 } ) )
43 42 eleq1i 
 |-  ( ( `' A " NN ) e. Fin <-> ( `' A " ( NN0 \ { 0 } ) ) e. Fin )
44 40 43 bitr4di 
 |-  ( A e. ( T i^i R ) -> ( ( `' A " ( _V \ { 0 } ) ) e. Fin <-> ( `' A " NN ) e. Fin ) )
45 32 44 mpbird 
 |-  ( A e. ( T i^i R ) -> ( `' A " ( _V \ { 0 } ) ) e. Fin )
46 resss 
 |-  ( A |` J ) C_ A
47 cnvss 
 |-  ( ( A |` J ) C_ A -> `' ( A |` J ) C_ `' A )
48 imass1 
 |-  ( `' ( A |` J ) C_ `' A -> ( `' ( A |` J ) " ( _V \ { 0 } ) ) C_ ( `' A " ( _V \ { 0 } ) ) )
49 46 47 48 mp2b 
 |-  ( `' ( A |` J ) " ( _V \ { 0 } ) ) C_ ( `' A " ( _V \ { 0 } ) )
50 ssfi 
 |-  ( ( ( `' A " ( _V \ { 0 } ) ) e. Fin /\ ( `' ( A |` J ) " ( _V \ { 0 } ) ) C_ ( `' A " ( _V \ { 0 } ) ) ) -> ( `' ( A |` J ) " ( _V \ { 0 } ) ) e. Fin )
51 45 49 50 sylancl 
 |-  ( A e. ( T i^i R ) -> ( `' ( A |` J ) " ( _V \ { 0 } ) ) e. Fin )
52 cnvco 
 |-  `' ( bits o. ( A |` J ) ) = ( `' ( A |` J ) o. `' bits )
53 52 imaeq1i 
 |-  ( `' ( bits o. ( A |` J ) ) " ( _V \ { (/) } ) ) = ( ( `' ( A |` J ) o. `' bits ) " ( _V \ { (/) } ) )
54 imaco 
 |-  ( ( `' ( A |` J ) o. `' bits ) " ( _V \ { (/) } ) ) = ( `' ( A |` J ) " ( `' bits " ( _V \ { (/) } ) ) )
55 53 54 eqtri 
 |-  ( `' ( bits o. ( A |` J ) ) " ( _V \ { (/) } ) ) = ( `' ( A |` J ) " ( `' bits " ( _V \ { (/) } ) ) )
56 ffun 
 |-  ( A : NN --> NN0 -> Fun A )
57 funres 
 |-  ( Fun A -> Fun ( A |` J ) )
58 20 56 57 3syl 
 |-  ( A e. ( T i^i R ) -> Fun ( A |` J ) )
59 ssv 
 |-  ( `' bits " _V ) C_ _V
60 ssdif 
 |-  ( ( `' bits " _V ) C_ _V -> ( ( `' bits " _V ) \ ( `' bits " { (/) } ) ) C_ ( _V \ ( `' bits " { (/) } ) ) )
61 59 60 ax-mp 
 |-  ( ( `' bits " _V ) \ ( `' bits " { (/) } ) ) C_ ( _V \ ( `' bits " { (/) } ) )
62 bitsf 
 |-  bits : ZZ --> ~P NN0
63 ffun 
 |-  ( bits : ZZ --> ~P NN0 -> Fun bits )
64 difpreima 
 |-  ( Fun bits -> ( `' bits " ( _V \ { (/) } ) ) = ( ( `' bits " _V ) \ ( `' bits " { (/) } ) ) )
65 62 63 64 mp2b 
 |-  ( `' bits " ( _V \ { (/) } ) ) = ( ( `' bits " _V ) \ ( `' bits " { (/) } ) )
66 bitsf1 
 |-  bits : ZZ -1-1-> ~P NN0
67 0z 
 |-  0 e. ZZ
68 snssi 
 |-  ( 0 e. ZZ -> { 0 } C_ ZZ )
69 67 68 ax-mp 
 |-  { 0 } C_ ZZ
70 f1imacnv 
 |-  ( ( bits : ZZ -1-1-> ~P NN0 /\ { 0 } C_ ZZ ) -> ( `' bits " ( bits " { 0 } ) ) = { 0 } )
71 66 69 70 mp2an 
 |-  ( `' bits " ( bits " { 0 } ) ) = { 0 }
72 ffn 
 |-  ( bits : ZZ --> ~P NN0 -> bits Fn ZZ )
73 62 72 ax-mp 
 |-  bits Fn ZZ
74 fnsnfv 
 |-  ( ( bits Fn ZZ /\ 0 e. ZZ ) -> { ( bits ` 0 ) } = ( bits " { 0 } ) )
75 73 67 74 mp2an 
 |-  { ( bits ` 0 ) } = ( bits " { 0 } )
76 0bits 
 |-  ( bits ` 0 ) = (/)
77 76 sneqi 
 |-  { ( bits ` 0 ) } = { (/) }
78 75 77 eqtr3i 
 |-  ( bits " { 0 } ) = { (/) }
79 78 imaeq2i 
 |-  ( `' bits " ( bits " { 0 } ) ) = ( `' bits " { (/) } )
80 71 79 eqtr3i 
 |-  { 0 } = ( `' bits " { (/) } )
81 80 difeq2i 
 |-  ( _V \ { 0 } ) = ( _V \ ( `' bits " { (/) } ) )
82 61 65 81 3sstr4i 
 |-  ( `' bits " ( _V \ { (/) } ) ) C_ ( _V \ { 0 } )
83 sspreima 
 |-  ( ( Fun ( A |` J ) /\ ( `' bits " ( _V \ { (/) } ) ) C_ ( _V \ { 0 } ) ) -> ( `' ( A |` J ) " ( `' bits " ( _V \ { (/) } ) ) ) C_ ( `' ( A |` J ) " ( _V \ { 0 } ) ) )
84 58 82 83 sylancl 
 |-  ( A e. ( T i^i R ) -> ( `' ( A |` J ) " ( `' bits " ( _V \ { (/) } ) ) ) C_ ( `' ( A |` J ) " ( _V \ { 0 } ) ) )
85 55 84 eqsstrid 
 |-  ( A e. ( T i^i R ) -> ( `' ( bits o. ( A |` J ) ) " ( _V \ { (/) } ) ) C_ ( `' ( A |` J ) " ( _V \ { 0 } ) ) )
86 ssfi 
 |-  ( ( ( `' ( A |` J ) " ( _V \ { 0 } ) ) e. Fin /\ ( `' ( bits o. ( A |` J ) ) " ( _V \ { (/) } ) ) C_ ( `' ( A |` J ) " ( _V \ { 0 } ) ) ) -> ( `' ( bits o. ( A |` J ) ) " ( _V \ { (/) } ) ) e. Fin )
87 51 85 86 syl2anc 
 |-  ( A e. ( T i^i R ) -> ( `' ( bits o. ( A |` J ) ) " ( _V \ { (/) } ) ) e. Fin )
88 oveq1 
 |-  ( r = ( bits o. ( A |` J ) ) -> ( r supp (/) ) = ( ( bits o. ( A |` J ) ) supp (/) ) )
89 88 eleq1d 
 |-  ( r = ( bits o. ( A |` J ) ) -> ( ( r supp (/) ) e. Fin <-> ( ( bits o. ( A |` J ) ) supp (/) ) e. Fin ) )
90 89 6 elrab2 
 |-  ( ( bits o. ( A |` J ) ) e. H <-> ( ( bits o. ( A |` J ) ) e. ( ( ~P NN0 i^i Fin ) ^m J ) /\ ( ( bits o. ( A |` J ) ) supp (/) ) e. Fin ) )
91 zex 
 |-  ZZ e. _V
92 fex 
 |-  ( ( bits : ZZ --> ~P NN0 /\ ZZ e. _V ) -> bits e. _V )
93 62 91 92 mp2an 
 |-  bits e. _V
94 resexg 
 |-  ( A e. ( T i^i R ) -> ( A |` J ) e. _V )
95 coexg 
 |-  ( ( bits e. _V /\ ( A |` J ) e. _V ) -> ( bits o. ( A |` J ) ) e. _V )
96 93 94 95 sylancr 
 |-  ( A e. ( T i^i R ) -> ( bits o. ( A |` J ) ) e. _V )
97 0ex 
 |-  (/) e. _V
98 suppimacnv 
 |-  ( ( ( bits o. ( A |` J ) ) e. _V /\ (/) e. _V ) -> ( ( bits o. ( A |` J ) ) supp (/) ) = ( `' ( bits o. ( A |` J ) ) " ( _V \ { (/) } ) ) )
99 97 98 mpan2 
 |-  ( ( bits o. ( A |` J ) ) e. _V -> ( ( bits o. ( A |` J ) ) supp (/) ) = ( `' ( bits o. ( A |` J ) ) " ( _V \ { (/) } ) ) )
100 99 eleq1d 
 |-  ( ( bits o. ( A |` J ) ) e. _V -> ( ( ( bits o. ( A |` J ) ) supp (/) ) e. Fin <-> ( `' ( bits o. ( A |` J ) ) " ( _V \ { (/) } ) ) e. Fin ) )
101 100 anbi2d 
 |-  ( ( bits o. ( A |` J ) ) e. _V -> ( ( ( bits o. ( A |` J ) ) e. ( ( ~P NN0 i^i Fin ) ^m J ) /\ ( ( bits o. ( A |` J ) ) supp (/) ) e. Fin ) <-> ( ( bits o. ( A |` J ) ) e. ( ( ~P NN0 i^i Fin ) ^m J ) /\ ( `' ( bits o. ( A |` J ) ) " ( _V \ { (/) } ) ) e. Fin ) ) )
102 96 101 syl 
 |-  ( A e. ( T i^i R ) -> ( ( ( bits o. ( A |` J ) ) e. ( ( ~P NN0 i^i Fin ) ^m J ) /\ ( ( bits o. ( A |` J ) ) supp (/) ) e. Fin ) <-> ( ( bits o. ( A |` J ) ) e. ( ( ~P NN0 i^i Fin ) ^m J ) /\ ( `' ( bits o. ( A |` J ) ) " ( _V \ { (/) } ) ) e. Fin ) ) )
103 90 102 syl5bb 
 |-  ( A e. ( T i^i R ) -> ( ( bits o. ( A |` J ) ) e. H <-> ( ( bits o. ( A |` J ) ) e. ( ( ~P NN0 i^i Fin ) ^m J ) /\ ( `' ( bits o. ( A |` J ) ) " ( _V \ { (/) } ) ) e. Fin ) ) )
104 31 87 103 mpbir2and 
 |-  ( A e. ( T i^i R ) -> ( bits o. ( A |` J ) ) e. H )