Metamath Proof Explorer

Theorem eulerpartlemn

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 30-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 ) ) ) ) ) )
eulerpart.s 
|- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
Assertion eulerpartlemn 
|- ( G |` O ) : O -1-1-onto-> D

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 eulerpart.s 
 |-  S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
12 simpl 
 |-  ( ( o = q /\ k e. NN ) -> o = q )
13 12 fveq1d 
 |-  ( ( o = q /\ k e. NN ) -> ( o ` k ) = ( q ` k ) )
14 13 oveq1d 
 |-  ( ( o = q /\ k e. NN ) -> ( ( o ` k ) x. k ) = ( ( q ` k ) x. k ) )
15 14 sumeq2dv 
 |-  ( o = q -> sum_ k e. NN ( ( o ` k ) x. k ) = sum_ k e. NN ( ( q ` k ) x. k ) )
16 15 eqeq1d 
 |-  ( o = q -> ( sum_ k e. NN ( ( o ` k ) x. k ) = N <-> sum_ k e. NN ( ( q ` k ) x. k ) = N ) )
17 16 cbvrabv 
 |-  { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } = { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N }
18 17 a1i 
 |-  ( o = q -> { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } = { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } )
19 18 reseq2d 
 |-  ( o = q -> ( G |` { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } ) = ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) )
20 eqidd 
 |-  ( o = q -> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } = { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } )
21 19 18 20 f1oeq123d 
 |-  ( o = q -> ( ( G |` { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } ) : { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } <-> ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) : { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } ) )
22 21 imbi2d 
 |-  ( o = q -> ( ( T. -> ( G |` { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } ) : { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } ) <-> ( T. -> ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) : { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } ) ) )
23 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 )
24 23 a1i 
 |-  ( T. -> G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) )
25 fveq2 
 |-  ( q = o -> ( G ` q ) = ( G ` o ) )
26 reseq1 
 |-  ( q = o -> ( q |` J ) = ( o |` J ) )
27 26 coeq2d 
 |-  ( q = o -> ( bits o. ( q |` J ) ) = ( bits o. ( o |` J ) ) )
28 27 fveq2d 
 |-  ( q = o -> ( M ` ( bits o. ( q |` J ) ) ) = ( M ` ( bits o. ( o |` J ) ) ) )
29 28 imaeq2d 
 |-  ( q = o -> ( F " ( M ` ( bits o. ( q |` J ) ) ) ) = ( F " ( M ` ( bits o. ( o |` J ) ) ) ) )
30 29 fveq2d 
 |-  ( q = o -> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( q |` J ) ) ) ) ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
31 25 30 eqeq12d 
 |-  ( q = o -> ( ( G ` q ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( q |` J ) ) ) ) ) <-> ( G ` o ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) )
32 1 2 3 4 5 6 7 8 9 10 eulerpartlemgv 
 |-  ( q e. ( T i^i R ) -> ( G ` q ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( q |` J ) ) ) ) ) )
33 31 32 vtoclga 
 |-  ( o e. ( T i^i R ) -> ( G ` o ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
34 33 3ad2ant2 
 |-  ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> ( G ` o ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
35 simp3 
 |-  ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
36 34 35 eqtr4d 
 |-  ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> ( G ` o ) = d )
37 36 fveq1d 
 |-  ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> ( ( G ` o ) ` k ) = ( d ` k ) )
38 37 oveq1d 
 |-  ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> ( ( ( G ` o ) ` k ) x. k ) = ( ( d ` k ) x. k ) )
39 38 sumeq2sdv 
 |-  ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> sum_ k e. NN ( ( ( G ` o ) ` k ) x. k ) = sum_ k e. NN ( ( d ` k ) x. k ) )
40 25 fveq2d 
 |-  ( q = o -> ( S ` ( G ` q ) ) = ( S ` ( G ` o ) ) )
41 fveq2 
 |-  ( q = o -> ( S ` q ) = ( S ` o ) )
42 40 41 eqeq12d 
 |-  ( q = o -> ( ( S ` ( G ` q ) ) = ( S ` q ) <-> ( S ` ( G ` o ) ) = ( S ` o ) ) )
43 1 2 3 4 5 6 7 8 9 10 11 eulerpartlemgs2 
 |-  ( q e. ( T i^i R ) -> ( S ` ( G ` q ) ) = ( S ` q ) )
44 42 43 vtoclga 
 |-  ( o e. ( T i^i R ) -> ( S ` ( G ` o ) ) = ( S ` o ) )
45 nn0ex 
 |-  NN0 e. _V
46 0nn0 
 |-  0 e. NN0
47 1nn0 
 |-  1 e. NN0
48 prssi 
 |-  ( ( 0 e. NN0 /\ 1 e. NN0 ) -> { 0 , 1 } C_ NN0 )
49 46 47 48 mp2an 
 |-  { 0 , 1 } C_ NN0
50 mapss 
 |-  ( ( NN0 e. _V /\ { 0 , 1 } C_ NN0 ) -> ( { 0 , 1 } ^m NN ) C_ ( NN0 ^m NN ) )
51 45 49 50 mp2an 
 |-  ( { 0 , 1 } ^m NN ) C_ ( NN0 ^m NN )
52 ssrin 
 |-  ( ( { 0 , 1 } ^m NN ) C_ ( NN0 ^m NN ) -> ( ( { 0 , 1 } ^m NN ) i^i R ) C_ ( ( NN0 ^m NN ) i^i R ) )
53 51 52 ax-mp 
 |-  ( ( { 0 , 1 } ^m NN ) i^i R ) C_ ( ( NN0 ^m NN ) i^i R )
54 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 ) )
55 23 54 ax-mp 
 |-  G : ( T i^i R ) --> ( ( { 0 , 1 } ^m NN ) i^i R )
56 55 ffvelrni 
 |-  ( o e. ( T i^i R ) -> ( G ` o ) e. ( ( { 0 , 1 } ^m NN ) i^i R ) )
57 53 56 sseldi 
 |-  ( o e. ( T i^i R ) -> ( G ` o ) e. ( ( NN0 ^m NN ) i^i R ) )
58 8 11 eulerpartlemsv1 
 |-  ( ( G ` o ) e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` ( G ` o ) ) = sum_ k e. NN ( ( ( G ` o ) ` k ) x. k ) )
59 57 58 syl 
 |-  ( o e. ( T i^i R ) -> ( S ` ( G ` o ) ) = sum_ k e. NN ( ( ( G ` o ) ` k ) x. k ) )
60 1 2 3 4 5 6 7 8 9 eulerpartlemt0 
 |-  ( o e. ( T i^i R ) <-> ( o e. ( NN0 ^m NN ) /\ ( `' o " NN ) e. Fin /\ ( `' o " NN ) C_ J ) )
61 60 simp1bi 
 |-  ( o e. ( T i^i R ) -> o e. ( NN0 ^m NN ) )
62 inss2 
 |-  ( T i^i R ) C_ R
63 62 sseli 
 |-  ( o e. ( T i^i R ) -> o e. R )
64 61 63 elind 
 |-  ( o e. ( T i^i R ) -> o e. ( ( NN0 ^m NN ) i^i R ) )
65 8 11 eulerpartlemsv1 
 |-  ( o e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` o ) = sum_ k e. NN ( ( o ` k ) x. k ) )
66 64 65 syl 
 |-  ( o e. ( T i^i R ) -> ( S ` o ) = sum_ k e. NN ( ( o ` k ) x. k ) )
67 44 59 66 3eqtr3d 
 |-  ( o e. ( T i^i R ) -> sum_ k e. NN ( ( ( G ` o ) ` k ) x. k ) = sum_ k e. NN ( ( o ` k ) x. k ) )
68 67 3ad2ant2 
 |-  ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> sum_ k e. NN ( ( ( G ` o ) ` k ) x. k ) = sum_ k e. NN ( ( o ` k ) x. k ) )
69 39 68 eqtr3d 
 |-  ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> sum_ k e. NN ( ( d ` k ) x. k ) = sum_ k e. NN ( ( o ` k ) x. k ) )
70 69 eqeq1d 
 |-  ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> ( sum_ k e. NN ( ( d ` k ) x. k ) = N <-> sum_ k e. NN ( ( o ` k ) x. k ) = N ) )
71 10 24 70 f1oresrab 
 |-  ( T. -> ( G |` { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } ) : { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } )
72 22 71 chvarvv 
 |-  ( T. -> ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) : { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } )
73 cnveq 
 |-  ( g = q -> `' g = `' q )
74 73 imaeq1d 
 |-  ( g = q -> ( `' g " NN ) = ( `' q " NN ) )
75 74 raleqdv 
 |-  ( g = q -> ( A. n e. ( `' g " NN ) -. 2 || n <-> A. n e. ( `' q " NN ) -. 2 || n ) )
76 75 cbvrabv 
 |-  { g e. P | A. n e. ( `' g " NN ) -. 2 || n } = { q e. P | A. n e. ( `' q " NN ) -. 2 || n }
77 nfrab1 
 |-  F/_ q { q e. P | A. n e. ( `' q " NN ) -. 2 || n }
78 nfrab1 
 |-  F/_ q { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N }
79 df-3an 
 |-  ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) <-> ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) )
80 79 anbi1i 
 |-  ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) /\ A. n e. ( `' q " NN ) -. 2 || n ) <-> ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) /\ A. n e. ( `' q " NN ) -. 2 || n ) )
81 1 eulerpartleme 
 |-  ( q e. P <-> ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) )
82 81 anbi1i 
 |-  ( ( q e. P /\ A. n e. ( `' q " NN ) -. 2 || n ) <-> ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) /\ A. n e. ( `' q " NN ) -. 2 || n ) )
83 an32 
 |-  ( ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ A. n e. ( `' q " NN ) -. 2 || n ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) <-> ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) /\ A. n e. ( `' q " NN ) -. 2 || n ) )
84 80 82 83 3bitr4i 
 |-  ( ( q e. P /\ A. n e. ( `' q " NN ) -. 2 || n ) <-> ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ A. n e. ( `' q " NN ) -. 2 || n ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) )
85 1 2 3 4 5 6 7 8 9 eulerpartlemt0 
 |-  ( q e. ( T i^i R ) <-> ( q e. ( NN0 ^m NN ) /\ ( `' q " NN ) e. Fin /\ ( `' q " NN ) C_ J ) )
86 nnex 
 |-  NN e. _V
87 45 86 elmap 
 |-  ( q e. ( NN0 ^m NN ) <-> q : NN --> NN0 )
88 87 3anbi1i 
 |-  ( ( q e. ( NN0 ^m NN ) /\ ( `' q " NN ) e. Fin /\ ( `' q " NN ) C_ J ) <-> ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ ( `' q " NN ) C_ J ) )
89 85 88 bitri 
 |-  ( q e. ( T i^i R ) <-> ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ ( `' q " NN ) C_ J ) )
90 df-3an 
 |-  ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ ( `' q " NN ) C_ J ) <-> ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ ( `' q " NN ) C_ J ) )
91 dfss3 
 |-  ( ( `' q " NN ) C_ J <-> A. n e. ( `' q " NN ) n e. J )
92 breq2 
 |-  ( z = n -> ( 2 || z <-> 2 || n ) )
93 92 notbid 
 |-  ( z = n -> ( -. 2 || z <-> -. 2 || n ) )
94 93 4 elrab2 
 |-  ( n e. J <-> ( n e. NN /\ -. 2 || n ) )
95 94 ralbii 
 |-  ( A. n e. ( `' q " NN ) n e. J <-> A. n e. ( `' q " NN ) ( n e. NN /\ -. 2 || n ) )
96 r19.26 
 |-  ( A. n e. ( `' q " NN ) ( n e. NN /\ -. 2 || n ) <-> ( A. n e. ( `' q " NN ) n e. NN /\ A. n e. ( `' q " NN ) -. 2 || n ) )
97 91 95 96 3bitri 
 |-  ( ( `' q " NN ) C_ J <-> ( A. n e. ( `' q " NN ) n e. NN /\ A. n e. ( `' q " NN ) -. 2 || n ) )
98 cnvimass 
 |-  ( `' q " NN ) C_ dom q
99 fdm 
 |-  ( q : NN --> NN0 -> dom q = NN )
100 98 99 sseqtrid 
 |-  ( q : NN --> NN0 -> ( `' q " NN ) C_ NN )
101 dfss3 
 |-  ( ( `' q " NN ) C_ NN <-> A. n e. ( `' q " NN ) n e. NN )
102 100 101 sylib 
 |-  ( q : NN --> NN0 -> A. n e. ( `' q " NN ) n e. NN )
103 102 biantrurd 
 |-  ( q : NN --> NN0 -> ( A. n e. ( `' q " NN ) -. 2 || n <-> ( A. n e. ( `' q " NN ) n e. NN /\ A. n e. ( `' q " NN ) -. 2 || n ) ) )
104 97 103 bitr4id 
 |-  ( q : NN --> NN0 -> ( ( `' q " NN ) C_ J <-> A. n e. ( `' q " NN ) -. 2 || n ) )
105 104 adantr 
 |-  ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) -> ( ( `' q " NN ) C_ J <-> A. n e. ( `' q " NN ) -. 2 || n ) )
106 105 pm5.32i 
 |-  ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ ( `' q " NN ) C_ J ) <-> ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ A. n e. ( `' q " NN ) -. 2 || n ) )
107 89 90 106 3bitri 
 |-  ( q e. ( T i^i R ) <-> ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ A. n e. ( `' q " NN ) -. 2 || n ) )
108 107 anbi1i 
 |-  ( ( q e. ( T i^i R ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) <-> ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ A. n e. ( `' q " NN ) -. 2 || n ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) )
109 84 108 bitr4i 
 |-  ( ( q e. P /\ A. n e. ( `' q " NN ) -. 2 || n ) <-> ( q e. ( T i^i R ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) )
110 rabid 
 |-  ( q e. { q e. P | A. n e. ( `' q " NN ) -. 2 || n } <-> ( q e. P /\ A. n e. ( `' q " NN ) -. 2 || n ) )
111 rabid 
 |-  ( q e. { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } <-> ( q e. ( T i^i R ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) )
112 109 110 111 3bitr4i 
 |-  ( q e. { q e. P | A. n e. ( `' q " NN ) -. 2 || n } <-> q e. { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } )
113 77 78 112 eqri 
 |-  { q e. P | A. n e. ( `' q " NN ) -. 2 || n } = { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N }
114 2 76 113 3eqtri 
 |-  O = { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N }
115 114 reseq2i 
 |-  ( G |` O ) = ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } )
116 115 a1i 
 |-  ( T. -> ( G |` O ) = ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) )
117 114 a1i 
 |-  ( T. -> O = { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } )
118 nfcv 
 |-  F/_ d D
119 nfrab1 
 |-  F/_ d { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N }
120 fnima 
 |-  ( d Fn NN -> ( d " NN ) = ran d )
121 120 sseq1d 
 |-  ( d Fn NN -> ( ( d " NN ) C_ { 0 , 1 } <-> ran d C_ { 0 , 1 } ) )
122 121 anbi2d 
 |-  ( d Fn NN -> ( ( ran d C_ NN0 /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ran d C_ NN0 /\ ran d C_ { 0 , 1 } ) ) )
123 sstr 
 |-  ( ( ran d C_ { 0 , 1 } /\ { 0 , 1 } C_ NN0 ) -> ran d C_ NN0 )
124 49 123 mpan2 
 |-  ( ran d C_ { 0 , 1 } -> ran d C_ NN0 )
125 124 pm4.71ri 
 |-  ( ran d C_ { 0 , 1 } <-> ( ran d C_ NN0 /\ ran d C_ { 0 , 1 } ) )
126 122 125 bitr4di 
 |-  ( d Fn NN -> ( ( ran d C_ NN0 /\ ( d " NN ) C_ { 0 , 1 } ) <-> ran d C_ { 0 , 1 } ) )
127 126 pm5.32i 
 |-  ( ( d Fn NN /\ ( ran d C_ NN0 /\ ( d " NN ) C_ { 0 , 1 } ) ) <-> ( d Fn NN /\ ran d C_ { 0 , 1 } ) )
128 anass 
 |-  ( ( ( d Fn NN /\ ran d C_ NN0 ) /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( d Fn NN /\ ( ran d C_ NN0 /\ ( d " NN ) C_ { 0 , 1 } ) ) )
129 df-f 
 |-  ( d : NN --> { 0 , 1 } <-> ( d Fn NN /\ ran d C_ { 0 , 1 } ) )
130 127 128 129 3bitr4ri 
 |-  ( d : NN --> { 0 , 1 } <-> ( ( d Fn NN /\ ran d C_ NN0 ) /\ ( d " NN ) C_ { 0 , 1 } ) )
131 prex 
 |-  { 0 , 1 } e. _V
132 131 86 elmap 
 |-  ( d e. ( { 0 , 1 } ^m NN ) <-> d : NN --> { 0 , 1 } )
133 df-f 
 |-  ( d : NN --> NN0 <-> ( d Fn NN /\ ran d C_ NN0 ) )
134 133 anbi1i 
 |-  ( ( d : NN --> NN0 /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ( d Fn NN /\ ran d C_ NN0 ) /\ ( d " NN ) C_ { 0 , 1 } ) )
135 130 132 134 3bitr4i 
 |-  ( d e. ( { 0 , 1 } ^m NN ) <-> ( d : NN --> NN0 /\ ( d " NN ) C_ { 0 , 1 } ) )
136 vex 
 |-  d e. _V
137 cnveq 
 |-  ( f = d -> `' f = `' d )
138 137 imaeq1d 
 |-  ( f = d -> ( `' f " NN ) = ( `' d " NN ) )
139 138 eleq1d 
 |-  ( f = d -> ( ( `' f " NN ) e. Fin <-> ( `' d " NN ) e. Fin ) )
140 136 139 8 elab2 
 |-  ( d e. R <-> ( `' d " NN ) e. Fin )
141 135 140 anbi12i 
 |-  ( ( d e. ( { 0 , 1 } ^m NN ) /\ d e. R ) <-> ( ( d : NN --> NN0 /\ ( d " NN ) C_ { 0 , 1 } ) /\ ( `' d " NN ) e. Fin ) )
142 elin 
 |-  ( d e. ( ( { 0 , 1 } ^m NN ) i^i R ) <-> ( d e. ( { 0 , 1 } ^m NN ) /\ d e. R ) )
143 an32 
 |-  ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ( d : NN --> NN0 /\ ( d " NN ) C_ { 0 , 1 } ) /\ ( `' d " NN ) e. Fin ) )
144 141 142 143 3bitr4i 
 |-  ( d e. ( ( { 0 , 1 } ^m NN ) i^i R ) <-> ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ ( d " NN ) C_ { 0 , 1 } ) )
145 144 anbi1i 
 |-  ( ( d e. ( ( { 0 , 1 } ^m NN ) i^i R ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) <-> ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ ( d " NN ) C_ { 0 , 1 } ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) )
146 1 eulerpartleme 
 |-  ( d e. P <-> ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) )
147 146 anbi1i 
 |-  ( ( d e. P /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) /\ ( d " NN ) C_ { 0 , 1 } ) )
148 df-3an 
 |-  ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) <-> ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) )
149 148 anbi1i 
 |-  ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) /\ ( d " NN ) C_ { 0 , 1 } ) )
150 an32 
 |-  ( ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ ( d " NN ) C_ { 0 , 1 } ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) )
151 147 149 150 3bitri 
 |-  ( ( d e. P /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ ( d " NN ) C_ { 0 , 1 } ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) )
152 145 151 bitr4i 
 |-  ( ( d e. ( ( { 0 , 1 } ^m NN ) i^i R ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) <-> ( d e. P /\ ( d " NN ) C_ { 0 , 1 } ) )
153 rabid 
 |-  ( d e. { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } <-> ( d e. ( ( { 0 , 1 } ^m NN ) i^i R ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) )
154 1 2 3 eulerpartlemd 
 |-  ( d e. D <-> ( d e. P /\ ( d " NN ) C_ { 0 , 1 } ) )
155 152 153 154 3bitr4ri 
 |-  ( d e. D <-> d e. { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } )
156 118 119 155 eqri 
 |-  D = { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N }
157 156 a1i 
 |-  ( T. -> D = { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } )
158 116 117 157 f1oeq123d 
 |-  ( T. -> ( ( G |` O ) : O -1-1-onto-> D <-> ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) : { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } ) )
159 72 158 mpbird 
 |-  ( T. -> ( G |` O ) : O -1-1-onto-> D )
160 159 mptru 
 |-  ( G |` O ) : O -1-1-onto-> D