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 \in (𝒫 ℕ_{0} \cap Fin) \to bits (\sum_{n \in A} 2^{n}) = A$

Proof

Step	Hyp	Ref	Expression
1		elinel2	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to A \in Fin$
2		2nn0	$⊢ 2 \in ℕ_{0}$
3	2	a1i	$⊢ (A \in (𝒫 ℕ_{0} \cap Fin) \land n \in A) \to 2 \in ℕ_{0}$
4		elfpw	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \leftrightarrow (A \subseteq ℕ_{0} \land A \in Fin)$
5	4	simplbi	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to A \subseteq ℕ_{0}$
6	5	sselda	$⊢ (A \in (𝒫 ℕ_{0} \cap Fin) \land n \in A) \to n \in ℕ_{0}$
7	3 6	nn0expcld	$⊢ (A \in (𝒫 ℕ_{0} \cap Fin) \land n \in A) \to 2^{n} \in ℕ_{0}$
8	1 7	fsumnn0cl	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to \sum_{n \in A} 2^{n} \in ℕ_{0}$
9		bitsinv1	$⊢ \sum_{n \in A} 2^{n} \in ℕ_{0} \to \sum_{m \in bits (\sum_{n \in A} 2^{n})} 2^{m} = \sum_{n \in A} 2^{n}$
10	8 9	syl	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to \sum_{m \in bits (\sum_{n \in A} 2^{n})} 2^{m} = \sum_{n \in A} 2^{n}$
11		bitsss	$⊢ bits (\sum_{n \in A} 2^{n}) \subseteq ℕ_{0}$
12	11	a1i	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to bits (\sum_{n \in A} 2^{n}) \subseteq ℕ_{0}$
13		bitsfi	$⊢ \sum_{n \in A} 2^{n} \in ℕ_{0} \to bits (\sum_{n \in A} 2^{n}) \in Fin$
14	8 13	syl	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to bits (\sum_{n \in A} 2^{n}) \in Fin$
15		elfpw	$⊢ bits (\sum_{n \in A} 2^{n}) \in (𝒫 ℕ_{0} \cap Fin) \leftrightarrow (bits (\sum_{n \in A} 2^{n}) \subseteq ℕ_{0} \land bits (\sum_{n \in A} 2^{n}) \in Fin)$
16	12 14 15	sylanbrc	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to bits (\sum_{n \in A} 2^{n}) \in (𝒫 ℕ_{0} \cap Fin)$
17		oveq2	$⊢ n = m \to 2^{n} = 2^{m}$
18	17	cbvsumv	$⊢ \sum_{n \in k} 2^{n} = \sum_{m \in k} 2^{m}$
19		sumeq1	$⊢ k = bits (\sum_{n \in A} 2^{n}) \to \sum_{m \in k} 2^{m} = \sum_{m \in bits (\sum_{n \in A} 2^{n})} 2^{m}$
20	18 19	eqtrid	$⊢ k = bits (\sum_{n \in A} 2^{n}) \to \sum_{n \in k} 2^{n} = \sum_{m \in bits (\sum_{n \in A} 2^{n})} 2^{m}$
21		eqid	$⊢ (k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) = (k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n})$
22		sumex	$⊢ \sum_{m \in bits (\sum_{n \in A} 2^{n})} 2^{m} \in V$
23	20 21 22	fvmpt	$⊢ bits (\sum_{n \in A} 2^{n}) \in (𝒫 ℕ_{0} \cap Fin) \to (k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) (bits (\sum_{n \in A} 2^{n})) = \sum_{m \in bits (\sum_{n \in A} 2^{n})} 2^{m}$
24	16 23	syl	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to (k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) (bits (\sum_{n \in A} 2^{n})) = \sum_{m \in bits (\sum_{n \in A} 2^{n})} 2^{m}$
25		sumeq1	$⊢ k = A \to \sum_{n \in k} 2^{n} = \sum_{n \in A} 2^{n}$
26		sumex	$⊢ \sum_{n \in A} 2^{n} \in V$
27	25 21 26	fvmpt	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to (k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) (A) = \sum_{n \in A} 2^{n}$
28	10 24 27	3eqtr4d	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to (k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) (bits (\sum_{n \in A} 2^{n})) = (k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) (A)$
29	21	ackbijnn	$⊢ (k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0}$
30		f1of1	$⊢ (k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0} \to (k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) : 𝒫 ℕ_{0} \cap Fin \underset{1-1}{⟶} ℕ_{0}$
31	29 30	mp1i	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to (k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) : 𝒫 ℕ_{0} \cap Fin \underset{1-1}{⟶} ℕ_{0}$
32		id	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to A \in (𝒫 ℕ_{0} \cap Fin)$
33		f1fveq	$⊢ ((k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) : 𝒫 ℕ_{0} \cap Fin \underset{1-1}{⟶} ℕ_{0} \land (bits (\sum_{n \in A} 2^{n}) \in (𝒫 ℕ_{0} \cap Fin) \land A \in (𝒫 ℕ_{0} \cap Fin))) \to ((k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) (bits (\sum_{n \in A} 2^{n})) = (k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) (A) \leftrightarrow bits (\sum_{n \in A} 2^{n}) = A)$
34	31 16 32 33	syl12anc	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to ((k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) (bits (\sum_{n \in A} 2^{n})) = (k \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in k} 2^{n}) (A) \leftrightarrow bits (\sum_{n \in A} 2^{n}) = A)$
35	28 34	mpbid	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to bits (\sum_{n \in A} 2^{n}) = A$

Metamath Proof Explorer

Theorem bitsinv2

Proof