Metamath Proof Explorer

Theorem eulerpartlemgf

Description: Lemma for eulerpart : Images under G have finite support. (Contributed by Thierry Arnoux, 29-Aug-2018)

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 eulerpartlemgf 
|- ( A e. ( T i^i R ) -> ( `' ( G ` A ) " NN ) e. Fin )

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 1 2 3 4 5 6 7 8 9 10 eulerpartlemgv 
 |-  ( A e. ( T i^i R ) -> ( G ` A ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) )
12 11 cnveqd 
 |-  ( A e. ( T i^i R ) -> `' ( G ` A ) = `' ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) )
13 12 imaeq1d 
 |-  ( A e. ( T i^i R ) -> ( `' ( G ` A ) " { 1 } ) = ( `' ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) " { 1 } ) )
14 nnex 
 |-  NN e. _V
15 imassrn 
 |-  ( F " ( M ` ( bits o. ( A |` J ) ) ) ) C_ ran F
16 4 5 oddpwdc 
 |-  F : ( J X. NN0 ) -1-1-onto-> NN
17 f1of 
 |-  ( F : ( J X. NN0 ) -1-1-onto-> NN -> F : ( J X. NN0 ) --> NN )
18 frn 
 |-  ( F : ( J X. NN0 ) --> NN -> ran F C_ NN )
19 16 17 18 mp2b 
 |-  ran F C_ NN
20 15 19 sstri 
 |-  ( F " ( M ` ( bits o. ( A |` J ) ) ) ) C_ NN
21 indpi1 
 |-  ( ( NN e. _V /\ ( F " ( M ` ( bits o. ( A |` J ) ) ) ) C_ NN ) -> ( `' ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) " { 1 } ) = ( F " ( M ` ( bits o. ( A |` J ) ) ) ) )
22 14 20 21 mp2an 
 |-  ( `' ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) " { 1 } ) = ( F " ( M ` ( bits o. ( A |` J ) ) ) )
23 13 22 eqtrdi 
 |-  ( A e. ( T i^i R ) -> ( `' ( G ` A ) " { 1 } ) = ( F " ( M ` ( bits o. ( A |` J ) ) ) ) )
24 ffun 
 |-  ( F : ( J X. NN0 ) --> NN -> Fun F )
25 16 17 24 mp2b 
 |-  Fun F
26 inss2 
 |-  ( ~P ( J X. NN0 ) i^i Fin ) C_ Fin
27 1 2 3 4 5 6 7 8 9 10 eulerpartlemmf 
 |-  ( A e. ( T i^i R ) -> ( bits o. ( A |` J ) ) e. H )
28 1 2 3 4 5 6 7 eulerpartlem1 
 |-  M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
29 f1of 
 |-  ( M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) -> M : H --> ( ~P ( J X. NN0 ) i^i Fin ) )
30 28 29 ax-mp 
 |-  M : H --> ( ~P ( J X. NN0 ) i^i Fin )
31 30 ffvelrni 
 |-  ( ( bits o. ( A |` J ) ) e. H -> ( M ` ( bits o. ( A |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
32 27 31 syl 
 |-  ( A e. ( T i^i R ) -> ( M ` ( bits o. ( A |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
33 26 32 sselid 
 |-  ( A e. ( T i^i R ) -> ( M ` ( bits o. ( A |` J ) ) ) e. Fin )
34 imafi 
 |-  ( ( Fun F /\ ( M ` ( bits o. ( A |` J ) ) ) e. Fin ) -> ( F " ( M ` ( bits o. ( A |` J ) ) ) ) e. Fin )
35 25 33 34 sylancr 
 |-  ( A e. ( T i^i R ) -> ( F " ( M ` ( bits o. ( A |` J ) ) ) ) e. Fin )
36 23 35 eqeltrd 
 |-  ( A e. ( T i^i R ) -> ( `' ( G ` A ) " { 1 } ) e. Fin )
37 1 2 3 4 5 6 7 8 9 10 eulerpartgbij 
 |-  G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )
38 f1of 
 |-  ( G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) -> G : ( T i^i R ) --> ( ( { 0 , 1 } ^m NN ) i^i R ) )
39 37 38 ax-mp 
 |-  G : ( T i^i R ) --> ( ( { 0 , 1 } ^m NN ) i^i R )
40 39 ffvelrni 
 |-  ( A e. ( T i^i R ) -> ( G ` A ) e. ( ( { 0 , 1 } ^m NN ) i^i R ) )
41 elin 
 |-  ( ( G ` A ) e. ( ( { 0 , 1 } ^m NN ) i^i R ) <-> ( ( G ` A ) e. ( { 0 , 1 } ^m NN ) /\ ( G ` A ) e. R ) )
42 41 simplbi 
 |-  ( ( G ` A ) e. ( ( { 0 , 1 } ^m NN ) i^i R ) -> ( G ` A ) e. ( { 0 , 1 } ^m NN ) )
43 elmapi 
 |-  ( ( G ` A ) e. ( { 0 , 1 } ^m NN ) -> ( G ` A ) : NN --> { 0 , 1 } )
44 40 42 43 3syl 
 |-  ( A e. ( T i^i R ) -> ( G ` A ) : NN --> { 0 , 1 } )
45 44 ffund 
 |-  ( A e. ( T i^i R ) -> Fun ( G ` A ) )
46 ssv 
 |-  NN0 C_ _V
47 dfn2 
 |-  NN = ( NN0 \ { 0 } )
48 ssdif 
 |-  ( NN0 C_ _V -> ( NN0 \ { 0 } ) C_ ( _V \ { 0 } ) )
49 47 48 eqsstrid 
 |-  ( NN0 C_ _V -> NN C_ ( _V \ { 0 } ) )
50 46 49 ax-mp 
 |-  NN C_ ( _V \ { 0 } )
51 sspreima 
 |-  ( ( Fun ( G ` A ) /\ NN C_ ( _V \ { 0 } ) ) -> ( `' ( G ` A ) " NN ) C_ ( `' ( G ` A ) " ( _V \ { 0 } ) ) )
52 45 50 51 sylancl 
 |-  ( A e. ( T i^i R ) -> ( `' ( G ` A ) " NN ) C_ ( `' ( G ` A ) " ( _V \ { 0 } ) ) )
53 fvex 
 |-  ( G ` A ) e. _V
54 0nn0 
 |-  0 e. NN0
55 suppimacnv 
 |-  ( ( ( G ` A ) e. _V /\ 0 e. NN0 ) -> ( ( G ` A ) supp 0 ) = ( `' ( G ` A ) " ( _V \ { 0 } ) ) )
56 53 54 55 mp2an 
 |-  ( ( G ` A ) supp 0 ) = ( `' ( G ` A ) " ( _V \ { 0 } ) )
57 0ne1 
 |-  0 =/= 1
58 difprsn1 
 |-  ( 0 =/= 1 -> ( { 0 , 1 } \ { 0 } ) = { 1 } )
59 57 58 ax-mp 
 |-  ( { 0 , 1 } \ { 0 } ) = { 1 }
60 59 eqcomi 
 |-  { 1 } = ( { 0 , 1 } \ { 0 } )
61 60 ffs2 
 |-  ( ( NN e. _V /\ 0 e. NN0 /\ ( G ` A ) : NN --> { 0 , 1 } ) -> ( ( G ` A ) supp 0 ) = ( `' ( G ` A ) " { 1 } ) )
62 14 54 61 mp3an12 
 |-  ( ( G ` A ) : NN --> { 0 , 1 } -> ( ( G ` A ) supp 0 ) = ( `' ( G ` A ) " { 1 } ) )
63 44 62 syl 
 |-  ( A e. ( T i^i R ) -> ( ( G ` A ) supp 0 ) = ( `' ( G ` A ) " { 1 } ) )
64 56 63 eqtr3id 
 |-  ( A e. ( T i^i R ) -> ( `' ( G ` A ) " ( _V \ { 0 } ) ) = ( `' ( G ` A ) " { 1 } ) )
65 52 64 sseqtrd 
 |-  ( A e. ( T i^i R ) -> ( `' ( G ` A ) " NN ) C_ ( `' ( G ` A ) " { 1 } ) )
66 ssfi 
 |-  ( ( ( `' ( G ` A ) " { 1 } ) e. Fin /\ ( `' ( G ` A ) " NN ) C_ ( `' ( G ` A ) " { 1 } ) ) -> ( `' ( G ` A ) " NN ) e. Fin )
67 36 65 66 syl2anc 
 |-  ( A e. ( T i^i R ) -> ( `' ( G ` A ) " NN ) e. Fin )