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 ↑ 𝑘 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitsinv.k | ⊢ 𝐾 = ◡ ( bits ↾ ℕ0 ) | |
2 | sumeq1 | ⊢ ( 𝑥 = 𝐴 → Σ 𝑘 ∈ 𝑥 ( 2 ↑ 𝑘 ) = Σ 𝑘 ∈ 𝐴 ( 2 ↑ 𝑘 ) ) | |
3 | bitsf1ocnv | ⊢ ( ( bits ↾ ℕ0 ) : ℕ0 –1-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 ↑ 𝑘 ) ) |