Metamath Proof Explorer

Theorem eulerpartlemt

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 19-Sep-2017)

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 }
Assertion eulerpartlemt 
|- ( ( NN0 ^m J ) i^i R ) = ran ( m e. ( T i^i R ) |-> ( m |` J ) )

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 elmapi 
 |-  ( o e. ( NN0 ^m J ) -> o : J --> NN0 )
11 10 adantr 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> o : J --> NN0 )
12 c0ex 
 |-  0 e. _V
13 12 fconst 
 |-  ( ( NN \ J ) X. { 0 } ) : ( NN \ J ) --> { 0 }
14 13 a1i 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( ( NN \ J ) X. { 0 } ) : ( NN \ J ) --> { 0 } )
15 disjdif 
 |-  ( J i^i ( NN \ J ) ) = (/)
16 15 a1i 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( J i^i ( NN \ J ) ) = (/) )
17 fun 
 |-  ( ( ( o : J --> NN0 /\ ( ( NN \ J ) X. { 0 } ) : ( NN \ J ) --> { 0 } ) /\ ( J i^i ( NN \ J ) ) = (/) ) -> ( o u. ( ( NN \ J ) X. { 0 } ) ) : ( J u. ( NN \ J ) ) --> ( NN0 u. { 0 } ) )
18 11 14 16 17 syl21anc 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( o u. ( ( NN \ J ) X. { 0 } ) ) : ( J u. ( NN \ J ) ) --> ( NN0 u. { 0 } ) )
19 ssrab2 
 |-  { z e. NN | -. 2 || z } C_ NN
20 4 19 eqsstri 
 |-  J C_ NN
21 undif 
 |-  ( J C_ NN <-> ( J u. ( NN \ J ) ) = NN )
22 20 21 mpbi 
 |-  ( J u. ( NN \ J ) ) = NN
23 0nn0 
 |-  0 e. NN0
24 snssi 
 |-  ( 0 e. NN0 -> { 0 } C_ NN0 )
25 23 24 ax-mp 
 |-  { 0 } C_ NN0
26 ssequn2 
 |-  ( { 0 } C_ NN0 <-> ( NN0 u. { 0 } ) = NN0 )
27 25 26 mpbi 
 |-  ( NN0 u. { 0 } ) = NN0
28 22 27 feq23i 
 |-  ( ( o u. ( ( NN \ J ) X. { 0 } ) ) : ( J u. ( NN \ J ) ) --> ( NN0 u. { 0 } ) <-> ( o u. ( ( NN \ J ) X. { 0 } ) ) : NN --> NN0 )
29 18 28 sylib 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( o u. ( ( NN \ J ) X. { 0 } ) ) : NN --> NN0 )
30 nn0ex 
 |-  NN0 e. _V
31 nnex 
 |-  NN e. _V
32 30 31 elmap 
 |-  ( ( o u. ( ( NN \ J ) X. { 0 } ) ) e. ( NN0 ^m NN ) <-> ( o u. ( ( NN \ J ) X. { 0 } ) ) : NN --> NN0 )
33 29 32 sylibr 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( o u. ( ( NN \ J ) X. { 0 } ) ) e. ( NN0 ^m NN ) )
34 cnvun 
 |-  `' ( o u. ( ( NN \ J ) X. { 0 } ) ) = ( `' o u. `' ( ( NN \ J ) X. { 0 } ) )
35 34 imaeq1i 
 |-  ( `' ( o u. ( ( NN \ J ) X. { 0 } ) ) " NN ) = ( ( `' o u. `' ( ( NN \ J ) X. { 0 } ) ) " NN )
36 imaundir 
 |-  ( ( `' o u. `' ( ( NN \ J ) X. { 0 } ) ) " NN ) = ( ( `' o " NN ) u. ( `' ( ( NN \ J ) X. { 0 } ) " NN ) )
37 35 36 eqtri 
 |-  ( `' ( o u. ( ( NN \ J ) X. { 0 } ) ) " NN ) = ( ( `' o " NN ) u. ( `' ( ( NN \ J ) X. { 0 } ) " NN ) )
38 vex 
 |-  o e. _V
39 cnveq 
 |-  ( f = o -> `' f = `' o )
40 39 imaeq1d 
 |-  ( f = o -> ( `' f " NN ) = ( `' o " NN ) )
41 40 eleq1d 
 |-  ( f = o -> ( ( `' f " NN ) e. Fin <-> ( `' o " NN ) e. Fin ) )
42 38 41 8 elab2 
 |-  ( o e. R <-> ( `' o " NN ) e. Fin )
43 42 bilani 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( `' o " NN ) e. Fin )
44 cnvxp 
 |-  `' ( ( NN \ J ) X. { 0 } ) = ( { 0 } X. ( NN \ J ) )
45 44 dmeqi 
 |-  dom `' ( ( NN \ J ) X. { 0 } ) = dom ( { 0 } X. ( NN \ J ) )
46 2nn 
 |-  2 e. NN
47 2z 
 |-  2 e. ZZ
48 iddvds 
 |-  ( 2 e. ZZ -> 2 || 2 )
49 47 48 ax-mp 
 |-  2 || 2
50 breq2 
 |-  ( z = 2 -> ( 2 || z <-> 2 || 2 ) )
51 50 notbid 
 |-  ( z = 2 -> ( -. 2 || z <-> -. 2 || 2 ) )
52 51 4 elrab2 
 |-  ( 2 e. J <-> ( 2 e. NN /\ -. 2 || 2 ) )
53 52 simprbi 
 |-  ( 2 e. J -> -. 2 || 2 )
54 49 53 mt2 
 |-  -. 2 e. J
55 eldif 
 |-  ( 2 e. ( NN \ J ) <-> ( 2 e. NN /\ -. 2 e. J ) )
56 46 54 55 mpbir2an 
 |-  2 e. ( NN \ J )
57 ne0i 
 |-  ( 2 e. ( NN \ J ) -> ( NN \ J ) =/= (/) )
58 dmxp 
 |-  ( ( NN \ J ) =/= (/) -> dom ( { 0 } X. ( NN \ J ) ) = { 0 } )
59 56 57 58 mp2b 
 |-  dom ( { 0 } X. ( NN \ J ) ) = { 0 }
60 45 59 eqtri 
 |-  dom `' ( ( NN \ J ) X. { 0 } ) = { 0 }
61 60 ineq1i 
 |-  ( dom `' ( ( NN \ J ) X. { 0 } ) i^i NN ) = ( { 0 } i^i NN )
62 incom 
 |-  ( NN i^i { 0 } ) = ( { 0 } i^i NN )
63 0nnn 
 |-  -. 0 e. NN
64 disjsn 
 |-  ( ( NN i^i { 0 } ) = (/) <-> -. 0 e. NN )
65 63 64 mpbir 
 |-  ( NN i^i { 0 } ) = (/)
66 61 62 65 3eqtr2i 
 |-  ( dom `' ( ( NN \ J ) X. { 0 } ) i^i NN ) = (/)
67 imadisj 
 |-  ( ( `' ( ( NN \ J ) X. { 0 } ) " NN ) = (/) <-> ( dom `' ( ( NN \ J ) X. { 0 } ) i^i NN ) = (/) )
68 66 67 mpbir 
 |-  ( `' ( ( NN \ J ) X. { 0 } ) " NN ) = (/)
69 0fi 
 |-  (/) e. Fin
70 68 69 eqeltri 
 |-  ( `' ( ( NN \ J ) X. { 0 } ) " NN ) e. Fin
71 unfi 
 |-  ( ( ( `' o " NN ) e. Fin /\ ( `' ( ( NN \ J ) X. { 0 } ) " NN ) e. Fin ) -> ( ( `' o " NN ) u. ( `' ( ( NN \ J ) X. { 0 } ) " NN ) ) e. Fin )
72 43 70 71 sylancl 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( ( `' o " NN ) u. ( `' ( ( NN \ J ) X. { 0 } ) " NN ) ) e. Fin )
73 37 72 eqeltrid 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( `' ( o u. ( ( NN \ J ) X. { 0 } ) ) " NN ) e. Fin )
74 cnvimass 
 |-  ( `' o " NN ) C_ dom o
75 74 11 fssdm 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( `' o " NN ) C_ J )
76 0ss 
 |-  (/) C_ J
77 68 76 eqsstri 
 |-  ( `' ( ( NN \ J ) X. { 0 } ) " NN ) C_ J
78 77 a1i 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( `' ( ( NN \ J ) X. { 0 } ) " NN ) C_ J )
79 75 78 unssd 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( ( `' o " NN ) u. ( `' ( ( NN \ J ) X. { 0 } ) " NN ) ) C_ J )
80 37 79 eqsstrid 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( `' ( o u. ( ( NN \ J ) X. { 0 } ) ) " NN ) C_ J )
81 1 2 3 4 5 6 7 8 9 eulerpartlemt0 
 |-  ( ( o u. ( ( NN \ J ) X. { 0 } ) ) e. ( T i^i R ) <-> ( ( o u. ( ( NN \ J ) X. { 0 } ) ) e. ( NN0 ^m NN ) /\ ( `' ( o u. ( ( NN \ J ) X. { 0 } ) ) " NN ) e. Fin /\ ( `' ( o u. ( ( NN \ J ) X. { 0 } ) ) " NN ) C_ J ) )
82 33 73 80 81 syl3anbrc 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( o u. ( ( NN \ J ) X. { 0 } ) ) e. ( T i^i R ) )
83 resundir 
 |-  ( ( o u. ( ( NN \ J ) X. { 0 } ) ) |` J ) = ( ( o |` J ) u. ( ( ( NN \ J ) X. { 0 } ) |` J ) )
84 ffn 
 |-  ( o : J --> NN0 -> o Fn J )
85 fnresdm 
 |-  ( o Fn J -> ( o |` J ) = o )
86 disjdifr 
 |-  ( ( NN \ J ) i^i J ) = (/)
87 fnconstg 
 |-  ( 0 e. NN0 -> ( ( NN \ J ) X. { 0 } ) Fn ( NN \ J ) )
88 fnresdisj 
 |-  ( ( ( NN \ J ) X. { 0 } ) Fn ( NN \ J ) -> ( ( ( NN \ J ) i^i J ) = (/) <-> ( ( ( NN \ J ) X. { 0 } ) |` J ) = (/) ) )
89 23 87 88 mp2b 
 |-  ( ( ( NN \ J ) i^i J ) = (/) <-> ( ( ( NN \ J ) X. { 0 } ) |` J ) = (/) )
90 86 89 mpbi 
 |-  ( ( ( NN \ J ) X. { 0 } ) |` J ) = (/)
91 90 a1i 
 |-  ( o Fn J -> ( ( ( NN \ J ) X. { 0 } ) |` J ) = (/) )
92 85 91 uneq12d 
 |-  ( o Fn J -> ( ( o |` J ) u. ( ( ( NN \ J ) X. { 0 } ) |` J ) ) = ( o u. (/) ) )
93 11 84 92 3syl 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( ( o |` J ) u. ( ( ( NN \ J ) X. { 0 } ) |` J ) ) = ( o u. (/) ) )
94 un0 
 |-  ( o u. (/) ) = o
95 93 94 eqtrdi 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( ( o |` J ) u. ( ( ( NN \ J ) X. { 0 } ) |` J ) ) = o )
96 83 95 eqtr2id 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> o = ( ( o u. ( ( NN \ J ) X. { 0 } ) ) |` J ) )
97 reseq1 
 |-  ( m = ( o u. ( ( NN \ J ) X. { 0 } ) ) -> ( m |` J ) = ( ( o u. ( ( NN \ J ) X. { 0 } ) ) |` J ) )
98 97 rspceeqv 
 |-  ( ( ( o u. ( ( NN \ J ) X. { 0 } ) ) e. ( T i^i R ) /\ o = ( ( o u. ( ( NN \ J ) X. { 0 } ) ) |` J ) ) -> E. m e. ( T i^i R ) o = ( m |` J ) )
99 82 96 98 syl2anc 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> E. m e. ( T i^i R ) o = ( m |` J ) )
100 simpr 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> o = ( m |` J ) )
101 1 2 3 4 5 6 7 8 9 eulerpartlemt0 
 |-  ( m e. ( T i^i R ) <-> ( m e. ( NN0 ^m NN ) /\ ( `' m " NN ) e. Fin /\ ( `' m " NN ) C_ J ) )
102 101 birani 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( m e. ( NN0 ^m NN ) /\ ( `' m " NN ) e. Fin /\ ( `' m " NN ) C_ J ) )
103 102 simp1d 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> m e. ( NN0 ^m NN ) )
104 30 31 elmap 
 |-  ( m e. ( NN0 ^m NN ) <-> m : NN --> NN0 )
105 103 104 sylib 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> m : NN --> NN0 )
106 fssres 
 |-  ( ( m : NN --> NN0 /\ J C_ NN ) -> ( m |` J ) : J --> NN0 )
107 105 20 106 sylancl 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( m |` J ) : J --> NN0 )
108 4 31 rabex2 
 |-  J e. _V
109 30 108 elmap 
 |-  ( ( m |` J ) e. ( NN0 ^m J ) <-> ( m |` J ) : J --> NN0 )
110 107 109 sylibr 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( m |` J ) e. ( NN0 ^m J ) )
111 100 110 eqeltrd 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> o e. ( NN0 ^m J ) )
112 ffun 
 |-  ( m : NN --> NN0 -> Fun m )
113 respreima 
 |-  ( Fun m -> ( `' ( m |` J ) " NN ) = ( ( `' m " NN ) i^i J ) )
114 105 112 113 3syl 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( `' ( m |` J ) " NN ) = ( ( `' m " NN ) i^i J ) )
115 102 simp2d 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( `' m " NN ) e. Fin )
116 infi 
 |-  ( ( `' m " NN ) e. Fin -> ( ( `' m " NN ) i^i J ) e. Fin )
117 115 116 syl 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( ( `' m " NN ) i^i J ) e. Fin )
118 114 117 eqeltrd 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( `' ( m |` J ) " NN ) e. Fin )
119 vex 
 |-  m e. _V
120 119 resex 
 |-  ( m |` J ) e. _V
121 cnveq 
 |-  ( f = ( m |` J ) -> `' f = `' ( m |` J ) )
122 121 imaeq1d 
 |-  ( f = ( m |` J ) -> ( `' f " NN ) = ( `' ( m |` J ) " NN ) )
123 122 eleq1d 
 |-  ( f = ( m |` J ) -> ( ( `' f " NN ) e. Fin <-> ( `' ( m |` J ) " NN ) e. Fin ) )
124 120 123 8 elab2 
 |-  ( ( m |` J ) e. R <-> ( `' ( m |` J ) " NN ) e. Fin )
125 118 124 sylibr 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( m |` J ) e. R )
126 100 125 eqeltrd 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> o e. R )
127 111 126 jca 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( o e. ( NN0 ^m J ) /\ o e. R ) )
128 127 rexlimiva 
 |-  ( E. m e. ( T i^i R ) o = ( m |` J ) -> ( o e. ( NN0 ^m J ) /\ o e. R ) )
129 99 128 impbii 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) <-> E. m e. ( T i^i R ) o = ( m |` J ) )
130 129 abbii 
 |-  { o | ( o e. ( NN0 ^m J ) /\ o e. R ) } = { o | E. m e. ( T i^i R ) o = ( m |` J ) }
131 df-in 
 |-  ( ( NN0 ^m J ) i^i R ) = { o | ( o e. ( NN0 ^m J ) /\ o e. R ) }
132 eqid 
 |-  ( m e. ( T i^i R ) |-> ( m |` J ) ) = ( m e. ( T i^i R ) |-> ( m |` J ) )
133 132 rnmpt 
 |-  ran ( m e. ( T i^i R ) |-> ( m |` J ) ) = { o | E. m e. ( T i^i R ) o = ( m |` J ) }
134 130 131 133 3eqtr4i 
 |-  ( ( NN0 ^m J ) i^i R ) = ran ( m e. ( T i^i R ) |-> ( m |` J ) )