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 ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 elinel2 ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → 𝐴 ∈ Fin )
2 2nn0 ⊢ 2 ∈ ℕ0
3 2 a1i ⊢ ( ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑛 ∈ 𝐴 ) → 2 ∈ ℕ0 )
4 elfpw ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( 𝐴 ⊆ ℕ0 ∧ 𝐴 ∈ Fin ) )
5 4 simplbi ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → 𝐴 ⊆ ℕ0 )
6 5 sselda ⊢ ( ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑛 ∈ 𝐴 ) → 𝑛 ∈ ℕ0 )
7 3 6 nn0expcld ⊢ ( ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑛 ∈ 𝐴 ) → ( 2 ↑ 𝑛 ) ∈ ℕ0 )
8 1 7 fsumnn0cl ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ∈ ℕ0 )
9 bitsinv1 ⊢ ( Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ∈ ℕ0 → Σ 𝑚 ∈ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ( 2 ↑ 𝑚 ) = Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) )
10 8 9 syl ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → Σ 𝑚 ∈ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ( 2 ↑ 𝑚 ) = Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) )
11 bitsss ⊢ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ⊆ ℕ0
12 11 a1i ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ⊆ ℕ0 )
13 bitsfi ⊢ ( Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ∈ ℕ0 → ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ∈ Fin )
14 8 13 syl ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ∈ Fin )
15 elfpw ⊢ ( ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ⊆ ℕ0 ∧ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ∈ Fin ) )
16 12 14 15 sylanbrc ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
17 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑚 ) )
18 17 cbvsumv ⊢ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) = Σ 𝑚 ∈ 𝑘 ( 2 ↑ 𝑚 )
19 sumeq1 ⊢ ( 𝑘 = ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) → Σ 𝑚 ∈ 𝑘 ( 2 ↑ 𝑚 ) = Σ 𝑚 ∈ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ( 2 ↑ 𝑚 ) )
20 18 19 eqtrid ⊢ ( 𝑘 = ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) → Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) = Σ 𝑚 ∈ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ( 2 ↑ 𝑚 ) )
21 eqid ⊢ ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) = ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) )
22 sumex ⊢ Σ 𝑚 ∈ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ( 2 ↑ 𝑚 ) ∈ V
23 20 21 22 fvmpt ⊢ ( ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) ‘ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ) = Σ 𝑚 ∈ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ( 2 ↑ 𝑚 ) )
24 16 23 syl ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) ‘ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ) = Σ 𝑚 ∈ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ( 2 ↑ 𝑚 ) )
25 sumeq1 ⊢ ( 𝑘 = 𝐴 → Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) = Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) )
26 sumex ⊢ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ∈ V
27 25 21 26 fvmpt ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) ‘ 𝐴 ) = Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) )
28 10 24 27 3eqtr4d ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) ‘ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ) = ( ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) ‘ 𝐴 ) )
29 21 ackbijnn ⊢ ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0
30 f1of1 ⊢ ( ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 → ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1→ ℕ0 )
31 29 30 mp1i ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1→ ℕ0 )
32 id ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) )
33 f1fveq ⊢ ( ( ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1→ ℕ0 ∧ ( ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) ) ) → ( ( ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) ‘ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ) = ( ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) ‘ 𝐴 ) ↔ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) = 𝐴 ) )
34 31 16 32 33 syl12anc ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ( ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) ‘ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) ) = ( ( 𝑘 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑘 ( 2 ↑ 𝑛 ) ) ‘ 𝐴 ) ↔ ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) = 𝐴 ) )
35 28 34 mpbid ⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( bits ‘ Σ 𝑛 ∈ 𝐴 ( 2 ↑ 𝑛 ) ) = 𝐴 )