Metamath Proof Explorer

Theorem bitsinv2

Description: There is an explicit inverse to the bits function for nonnegative integers, part 2. (Contributed by Mario Carneiro, 8-Sep-2016)

Ref Expression
Assertion bitsinv2 
|- ( A e. ( ~P NN0 i^i Fin ) -> ( bits ` sum_ n e. A ( 2 ^ n ) ) = A )

Proof

Step Hyp Ref Expression
1 elinel2 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> A e. Fin )
2 2nn0 
 |-  2 e. NN0
3 2 a1i 
 |-  ( ( A e. ( ~P NN0 i^i Fin ) /\ n e. A ) -> 2 e. NN0 )
4 elfpw 
 |-  ( A e. ( ~P NN0 i^i Fin ) <-> ( A C_ NN0 /\ A e. Fin ) )
5 4 simplbi 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> A C_ NN0 )
6 5 sselda 
 |-  ( ( A e. ( ~P NN0 i^i Fin ) /\ n e. A ) -> n e. NN0 )
7 3 6 nn0expcld 
 |-  ( ( A e. ( ~P NN0 i^i Fin ) /\ n e. A ) -> ( 2 ^ n ) e. NN0 )
8 1 7 fsumnn0cl 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> sum_ n e. A ( 2 ^ n ) e. NN0 )
9 bitsinv1 
 |-  ( sum_ n e. A ( 2 ^ n ) e. NN0 -> sum_ m e. ( bits ` sum_ n e. A ( 2 ^ n ) ) ( 2 ^ m ) = sum_ n e. A ( 2 ^ n ) )
10 8 9 syl 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> sum_ m e. ( bits ` sum_ n e. A ( 2 ^ n ) ) ( 2 ^ m ) = sum_ n e. A ( 2 ^ n ) )
11 bitsss 
 |-  ( bits ` sum_ n e. A ( 2 ^ n ) ) C_ NN0
12 11 a1i 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> ( bits ` sum_ n e. A ( 2 ^ n ) ) C_ NN0 )
13 bitsfi 
 |-  ( sum_ n e. A ( 2 ^ n ) e. NN0 -> ( bits ` sum_ n e. A ( 2 ^ n ) ) e. Fin )
14 8 13 syl 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> ( bits ` sum_ n e. A ( 2 ^ n ) ) e. Fin )
15 elfpw 
 |-  ( ( bits ` sum_ n e. A ( 2 ^ n ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( bits ` sum_ n e. A ( 2 ^ n ) ) C_ NN0 /\ ( bits ` sum_ n e. A ( 2 ^ n ) ) e. Fin ) )
16 12 14 15 sylanbrc 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> ( bits ` sum_ n e. A ( 2 ^ n ) ) e. ( ~P NN0 i^i Fin ) )
17 oveq2 
 |-  ( n = m -> ( 2 ^ n ) = ( 2 ^ m ) )
18 17 cbvsumv 
 |-  sum_ n e. k ( 2 ^ n ) = sum_ m e. k ( 2 ^ m )
19 sumeq1 
 |-  ( k = ( bits ` sum_ n e. A ( 2 ^ n ) ) -> sum_ m e. k ( 2 ^ m ) = sum_ m e. ( bits ` sum_ n e. A ( 2 ^ n ) ) ( 2 ^ m ) )
20 18 19 syl5eq 
 |-  ( k = ( bits ` sum_ n e. A ( 2 ^ n ) ) -> sum_ n e. k ( 2 ^ n ) = sum_ m e. ( bits ` sum_ n e. A ( 2 ^ n ) ) ( 2 ^ m ) )
21 eqid 
 |-  ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) = ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) )
22 sumex 
 |-  sum_ m e. ( bits ` sum_ n e. A ( 2 ^ n ) ) ( 2 ^ m ) e. _V
23 20 21 22 fvmpt 
 |-  ( ( bits ` sum_ n e. A ( 2 ^ n ) ) e. ( ~P NN0 i^i Fin ) -> ( ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) ` ( bits ` sum_ n e. A ( 2 ^ n ) ) ) = sum_ m e. ( bits ` sum_ n e. A ( 2 ^ n ) ) ( 2 ^ m ) )
24 16 23 syl 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> ( ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) ` ( bits ` sum_ n e. A ( 2 ^ n ) ) ) = sum_ m e. ( bits ` sum_ n e. A ( 2 ^ n ) ) ( 2 ^ m ) )
25 sumeq1 
 |-  ( k = A -> sum_ n e. k ( 2 ^ n ) = sum_ n e. A ( 2 ^ n ) )
26 sumex 
 |-  sum_ n e. A ( 2 ^ n ) e. _V
27 25 21 26 fvmpt 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> ( ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) ` A ) = sum_ n e. A ( 2 ^ n ) )
28 10 24 27 3eqtr4d 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> ( ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) ` ( bits ` sum_ n e. A ( 2 ^ n ) ) ) = ( ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) ` A ) )
29 21 ackbijnn 
 |-  ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0
30 f1of1 
 |-  ( ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 -> ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) : ( ~P NN0 i^i Fin ) -1-1-> NN0 )
31 29 30 mp1i 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) : ( ~P NN0 i^i Fin ) -1-1-> NN0 )
32 id 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> A e. ( ~P NN0 i^i Fin ) )
33 f1fveq 
 |-  ( ( ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) : ( ~P NN0 i^i Fin ) -1-1-> NN0 /\ ( ( bits ` sum_ n e. A ( 2 ^ n ) ) e. ( ~P NN0 i^i Fin ) /\ A e. ( ~P NN0 i^i Fin ) ) ) -> ( ( ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) ` ( bits ` sum_ n e. A ( 2 ^ n ) ) ) = ( ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) ` A ) <-> ( bits ` sum_ n e. A ( 2 ^ n ) ) = A ) )
34 31 16 32 33 syl12anc 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> ( ( ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) ` ( bits ` sum_ n e. A ( 2 ^ n ) ) ) = ( ( k e. ( ~P NN0 i^i Fin ) |-> sum_ n e. k ( 2 ^ n ) ) ` A ) <-> ( bits ` sum_ n e. A ( 2 ^ n ) ) = A ) )
35 28 34 mpbid 
 |-  ( A e. ( ~P NN0 i^i Fin ) -> ( bits ` sum_ n e. A ( 2 ^ n ) ) = A )