Metamath Proof Explorer

Theorem eulerpartlemgu

Description: Lemma for eulerpart : Rewriting the U set for an odd partition Note that interestingly, this proof reuses marypha2lem2 . (Contributed by Thierry Arnoux, 10-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 ) ) ) ) ) )
eulerpartlemgh.1 
|- U = U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) )
Assertion eulerpartlemgu 
|- ( A e. ( T i^i R ) -> U = { <. t , n >. | ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( ( bits o. A ) ` t ) ) } )

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 eulerpartlemgh.1 
 |-  U = U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) )
12 eqid 
 |-  U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( ( bits o. A ) ` t ) ) = U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( ( bits o. A ) ` t ) )
13 12 marypha2lem2 
 |-  U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( ( bits o. A ) ` t ) ) = { <. t , n >. | ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( ( bits o. A ) ` t ) ) }
14 1 2 3 4 5 6 7 8 9 eulerpartlemt0 
 |-  ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )
15 14 simp1bi 
 |-  ( A e. ( T i^i R ) -> A e. ( NN0 ^m NN ) )
16 elmapi 
 |-  ( A e. ( NN0 ^m NN ) -> A : NN --> NN0 )
17 15 16 syl 
 |-  ( A e. ( T i^i R ) -> A : NN --> NN0 )
18 17 adantr 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> A : NN --> NN0 )
19 18 ffund 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> Fun A )
20 inss1 
 |-  ( ( `' A " NN ) i^i J ) C_ ( `' A " NN )
21 cnvimass 
 |-  ( `' A " NN ) C_ dom A
22 21 17 fssdm 
 |-  ( A e. ( T i^i R ) -> ( `' A " NN ) C_ NN )
23 20 22 sstrid 
 |-  ( A e. ( T i^i R ) -> ( ( `' A " NN ) i^i J ) C_ NN )
24 23 sselda 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> t e. NN )
25 17 fdmd 
 |-  ( A e. ( T i^i R ) -> dom A = NN )
26 25 eleq2d 
 |-  ( A e. ( T i^i R ) -> ( t e. dom A <-> t e. NN ) )
27 26 adantr 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> ( t e. dom A <-> t e. NN ) )
28 24 27 mpbird 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> t e. dom A )
29 fvco 
 |-  ( ( Fun A /\ t e. dom A ) -> ( ( bits o. A ) ` t ) = ( bits ` ( A ` t ) ) )
30 19 28 29 syl2anc 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> ( ( bits o. A ) ` t ) = ( bits ` ( A ` t ) ) )
31 30 xpeq2d 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> ( { t } X. ( ( bits o. A ) ` t ) ) = ( { t } X. ( bits ` ( A ` t ) ) ) )
32 31 iuneq2dv 
 |-  ( A e. ( T i^i R ) -> U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( ( bits o. A ) ` t ) ) = U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) )
33 13 32 syl5reqr 
 |-  ( A e. ( T i^i R ) -> U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) = { <. t , n >. | ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( ( bits o. A ) ` t ) ) } )
34 11 33 syl5eq 
 |-  ( A e. ( T i^i R ) -> U = { <. t , n >. | ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( ( bits o. A ) ` t ) ) } )