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 biimpi 
 |-  ( o e. R -> ( `' o " NN ) e. Fin )
44 43 adantl 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( `' o " NN ) e. Fin )
45 cnvxp 
 |-  `' ( ( NN \ J ) X. { 0 } ) = ( { 0 } X. ( NN \ J ) )
46 45 dmeqi 
 |-  dom `' ( ( NN \ J ) X. { 0 } ) = dom ( { 0 } X. ( NN \ J ) )
47 2nn 
 |-  2 e. NN
48 2z 
 |-  2 e. ZZ
49 iddvds 
 |-  ( 2 e. ZZ -> 2 || 2 )
50 48 49 ax-mp 
 |-  2 || 2
51 breq2 
 |-  ( z = 2 -> ( 2 || z <-> 2 || 2 ) )
52 51 notbid 
 |-  ( z = 2 -> ( -. 2 || z <-> -. 2 || 2 ) )
53 52 4 elrab2 
 |-  ( 2 e. J <-> ( 2 e. NN /\ -. 2 || 2 ) )
54 53 simprbi 
 |-  ( 2 e. J -> -. 2 || 2 )
55 50 54 mt2 
 |-  -. 2 e. J
56 eldif 
 |-  ( 2 e. ( NN \ J ) <-> ( 2 e. NN /\ -. 2 e. J ) )
57 47 55 56 mpbir2an 
 |-  2 e. ( NN \ J )
58 ne0i 
 |-  ( 2 e. ( NN \ J ) -> ( NN \ J ) =/= (/) )
59 dmxp 
 |-  ( ( NN \ J ) =/= (/) -> dom ( { 0 } X. ( NN \ J ) ) = { 0 } )
60 57 58 59 mp2b 
 |-  dom ( { 0 } X. ( NN \ J ) ) = { 0 }
61 46 60 eqtri 
 |-  dom `' ( ( NN \ J ) X. { 0 } ) = { 0 }
62 61 ineq1i 
 |-  ( dom `' ( ( NN \ J ) X. { 0 } ) i^i NN ) = ( { 0 } i^i NN )
63 incom 
 |-  ( NN i^i { 0 } ) = ( { 0 } i^i NN )
64 0nnn 
 |-  -. 0 e. NN
65 disjsn 
 |-  ( ( NN i^i { 0 } ) = (/) <-> -. 0 e. NN )
66 64 65 mpbir 
 |-  ( NN i^i { 0 } ) = (/)
67 62 63 66 3eqtr2i 
 |-  ( dom `' ( ( NN \ J ) X. { 0 } ) i^i NN ) = (/)
68 imadisj 
 |-  ( ( `' ( ( NN \ J ) X. { 0 } ) " NN ) = (/) <-> ( dom `' ( ( NN \ J ) X. { 0 } ) i^i NN ) = (/) )
69 67 68 mpbir 
 |-  ( `' ( ( NN \ J ) X. { 0 } ) " NN ) = (/)
70 0fin 
 |-  (/) e. Fin
71 69 70 eqeltri 
 |-  ( `' ( ( NN \ J ) X. { 0 } ) " NN ) e. Fin
72 unfi 
 |-  ( ( ( `' o " NN ) e. Fin /\ ( `' ( ( NN \ J ) X. { 0 } ) " NN ) e. Fin ) -> ( ( `' o " NN ) u. ( `' ( ( NN \ J ) X. { 0 } ) " NN ) ) e. Fin )
73 44 71 72 sylancl 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( ( `' o " NN ) u. ( `' ( ( NN \ J ) X. { 0 } ) " NN ) ) e. Fin )
74 37 73 eqeltrid 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( `' ( o u. ( ( NN \ J ) X. { 0 } ) ) " NN ) e. Fin )
75 cnvimass 
 |-  ( `' o " NN ) C_ dom o
76 75 11 fssdm 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( `' o " NN ) C_ J )
77 0ss 
 |-  (/) C_ J
78 69 77 eqsstri 
 |-  ( `' ( ( NN \ J ) X. { 0 } ) " NN ) C_ J
79 78 a1i 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( `' ( ( NN \ J ) X. { 0 } ) " NN ) C_ J )
80 76 79 unssd 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( ( `' o " NN ) u. ( `' ( ( NN \ J ) X. { 0 } ) " NN ) ) C_ J )
81 37 80 eqsstrid 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( `' ( o u. ( ( NN \ J ) X. { 0 } ) ) " NN ) C_ J )
82 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 ) )
83 33 74 81 82 syl3anbrc 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( o u. ( ( NN \ J ) X. { 0 } ) ) e. ( T i^i R ) )
84 resundir 
 |-  ( ( o u. ( ( NN \ J ) X. { 0 } ) ) |` J ) = ( ( o |` J ) u. ( ( ( NN \ J ) X. { 0 } ) |` J ) )
85 ffn 
 |-  ( o : J --> NN0 -> o Fn J )
86 fnresdm 
 |-  ( o Fn J -> ( o |` J ) = o )
87 disjdifr 
 |-  ( ( NN \ J ) i^i J ) = (/)
88 fnconstg 
 |-  ( 0 e. NN0 -> ( ( NN \ J ) X. { 0 } ) Fn ( NN \ J ) )
89 fnresdisj 
 |-  ( ( ( NN \ J ) X. { 0 } ) Fn ( NN \ J ) -> ( ( ( NN \ J ) i^i J ) = (/) <-> ( ( ( NN \ J ) X. { 0 } ) |` J ) = (/) ) )
90 23 88 89 mp2b 
 |-  ( ( ( NN \ J ) i^i J ) = (/) <-> ( ( ( NN \ J ) X. { 0 } ) |` J ) = (/) )
91 87 90 mpbi 
 |-  ( ( ( NN \ J ) X. { 0 } ) |` J ) = (/)
92 91 a1i 
 |-  ( o Fn J -> ( ( ( NN \ J ) X. { 0 } ) |` J ) = (/) )
93 86 92 uneq12d 
 |-  ( o Fn J -> ( ( o |` J ) u. ( ( ( NN \ J ) X. { 0 } ) |` J ) ) = ( o u. (/) ) )
94 11 85 93 3syl 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( ( o |` J ) u. ( ( ( NN \ J ) X. { 0 } ) |` J ) ) = ( o u. (/) ) )
95 un0 
 |-  ( o u. (/) ) = o
96 94 95 eqtrdi 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> ( ( o |` J ) u. ( ( ( NN \ J ) X. { 0 } ) |` J ) ) = o )
97 84 96 eqtr2id 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> o = ( ( o u. ( ( NN \ J ) X. { 0 } ) ) |` J ) )
98 reseq1 
 |-  ( m = ( o u. ( ( NN \ J ) X. { 0 } ) ) -> ( m |` J ) = ( ( o u. ( ( NN \ J ) X. { 0 } ) ) |` J ) )
99 98 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 ) )
100 83 97 99 syl2anc 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) -> E. m e. ( T i^i R ) o = ( m |` J ) )
101 simpr 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> o = ( m |` J ) )
102 simpl 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> m e. ( T i^i R ) )
103 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 ) )
104 102 103 sylib 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( m e. ( NN0 ^m NN ) /\ ( `' m " NN ) e. Fin /\ ( `' m " NN ) C_ J ) )
105 104 simp1d 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> m e. ( NN0 ^m NN ) )
106 30 31 elmap 
 |-  ( m e. ( NN0 ^m NN ) <-> m : NN --> NN0 )
107 105 106 sylib 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> m : NN --> NN0 )
108 fssres 
 |-  ( ( m : NN --> NN0 /\ J C_ NN ) -> ( m |` J ) : J --> NN0 )
109 107 20 108 sylancl 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( m |` J ) : J --> NN0 )
110 4 31 rabex2 
 |-  J e. _V
111 30 110 elmap 
 |-  ( ( m |` J ) e. ( NN0 ^m J ) <-> ( m |` J ) : J --> NN0 )
112 109 111 sylibr 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( m |` J ) e. ( NN0 ^m J ) )
113 101 112 eqeltrd 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> o e. ( NN0 ^m J ) )
114 ffun 
 |-  ( m : NN --> NN0 -> Fun m )
115 respreima 
 |-  ( Fun m -> ( `' ( m |` J ) " NN ) = ( ( `' m " NN ) i^i J ) )
116 107 114 115 3syl 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( `' ( m |` J ) " NN ) = ( ( `' m " NN ) i^i J ) )
117 104 simp2d 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( `' m " NN ) e. Fin )
118 infi 
 |-  ( ( `' m " NN ) e. Fin -> ( ( `' m " NN ) i^i J ) e. Fin )
119 117 118 syl 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( ( `' m " NN ) i^i J ) e. Fin )
120 116 119 eqeltrd 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( `' ( m |` J ) " NN ) e. Fin )
121 vex 
 |-  m e. _V
122 121 resex 
 |-  ( m |` J ) e. _V
123 cnveq 
 |-  ( f = ( m |` J ) -> `' f = `' ( m |` J ) )
124 123 imaeq1d 
 |-  ( f = ( m |` J ) -> ( `' f " NN ) = ( `' ( m |` J ) " NN ) )
125 124 eleq1d 
 |-  ( f = ( m |` J ) -> ( ( `' f " NN ) e. Fin <-> ( `' ( m |` J ) " NN ) e. Fin ) )
126 122 125 8 elab2 
 |-  ( ( m |` J ) e. R <-> ( `' ( m |` J ) " NN ) e. Fin )
127 120 126 sylibr 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( m |` J ) e. R )
128 101 127 eqeltrd 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> o e. R )
129 113 128 jca 
 |-  ( ( m e. ( T i^i R ) /\ o = ( m |` J ) ) -> ( o e. ( NN0 ^m J ) /\ o e. R ) )
130 129 rexlimiva 
 |-  ( E. m e. ( T i^i R ) o = ( m |` J ) -> ( o e. ( NN0 ^m J ) /\ o e. R ) )
131 100 130 impbii 
 |-  ( ( o e. ( NN0 ^m J ) /\ o e. R ) <-> E. m e. ( T i^i R ) o = ( m |` J ) )
132 131 abbii 
 |-  { o | ( o e. ( NN0 ^m J ) /\ o e. R ) } = { o | E. m e. ( T i^i R ) o = ( m |` J ) }
133 df-in 
 |-  ( ( NN0 ^m J ) i^i R ) = { o | ( o e. ( NN0 ^m J ) /\ o e. R ) }
134 eqid 
 |-  ( m e. ( T i^i R ) |-> ( m |` J ) ) = ( m e. ( T i^i R ) |-> ( m |` J ) )
135 134 rnmpt 
 |-  ran ( m e. ( T i^i R ) |-> ( m |` J ) ) = { o | E. m e. ( T i^i R ) o = ( m |` J ) }
136 132 133 135 3eqtr4i 
 |-  ( ( NN0 ^m J ) i^i R ) = ran ( m e. ( T i^i R ) |-> ( m |` J ) )