Metamath Proof Explorer


Theorem bitsinv

Description: The inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016)

Ref Expression
Hypothesis bitsinv.k 𝐾 = ( bits ↾ ℕ0 )
Assertion bitsinv ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝐾𝐴 ) = Σ 𝑘𝐴 ( 2 ↑ 𝑘 ) )

Proof

Step Hyp Ref Expression
1 bitsinv.k 𝐾 = ( bits ↾ ℕ0 )
2 sumeq1 ( 𝑥 = 𝐴 → Σ 𝑘𝑥 ( 2 ↑ 𝑘 ) = Σ 𝑘𝐴 ( 2 ↑ 𝑘 ) )
3 bitsf1ocnv ( ( bits ↾ ℕ0 ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( bits ↾ ℕ0 ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑘𝑥 ( 2 ↑ 𝑘 ) ) )
4 3 simpri ( bits ↾ ℕ0 ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑘𝑥 ( 2 ↑ 𝑘 ) )
5 1 4 eqtri 𝐾 = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑘𝑥 ( 2 ↑ 𝑘 ) )
6 sumex Σ 𝑘𝐴 ( 2 ↑ 𝑘 ) ∈ V
7 2 5 6 fvmpt ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝐾𝐴 ) = Σ 𝑘𝐴 ( 2 ↑ 𝑘 ) )