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 ) : ℕ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 ↑ 𝑘 ) )