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 sselid
 |-  ( 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