Theorem smufval

Description: The multiplication of two bit sequences as repeated sequence addition. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Hypotheses	smuval.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
	smuval.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
	smuval.p	$$⊢P=seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
Assertion	smufval	$$⊢\phi \to A\mathrm{smul}B=\left\{k\in {\mathbb{N}}_0|k\in P\left(k+1\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		smuval.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
2		smuval.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
3		smuval.p	$$⊢P=seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
4		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
5	4	elpw2	$$⊢A\in 𝒫{\mathbb{N}}_0\leftrightarrow A\subseteq {\mathbb{N}}_0$$
6	1 5	sylibr	$$⊢\phi \to A\in 𝒫{\mathbb{N}}_0$$
7	4	elpw2	$$⊢B\in 𝒫{\mathbb{N}}_0\leftrightarrow B\subseteq {\mathbb{N}}_0$$
8	2 7	sylibr	$$⊢\phi \to B\in 𝒫{\mathbb{N}}_0$$
9		simp1l	$$⊢\left(\left(x=A\wedge y=B\right)\wedge p\in 𝒫{\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to x=A$$
10	9	eleq2d	$$⊢\left(\left(x=A\wedge y=B\right)\wedge p\in 𝒫{\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to \left(m\in x\leftrightarrow m\in A\right)$$
11		simp1r	$$⊢\left(\left(x=A\wedge y=B\right)\wedge p\in 𝒫{\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to y=B$$
12	11	eleq2d	$$⊢\left(\left(x=A\wedge y=B\right)\wedge p\in 𝒫{\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to \left(n-m\in y\leftrightarrow n-m\in B\right)$$
13	10 12	anbi12d	$$⊢\left(\left(x=A\wedge y=B\right)\wedge p\in 𝒫{\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to \left(\left(m\in x\wedge n-m\in y\right)\leftrightarrow \left(m\in A\wedge n-m\in B\right)\right)$$
14	13	rabbidv	$$⊢\left(\left(x=A\wedge y=B\right)\wedge p\in 𝒫{\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to \left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}=\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}$$
15	14	oveq2d	$$⊢\left(\left(x=A\wedge y=B\right)\wedge p\in 𝒫{\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}=p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}$$
16	15	mpoeq3dva	$$⊢\left(x=A\wedge y=B\right)\to \left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}\right)=\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right)$$
17	16	seqeq2d	$$⊢\left(x=A\wedge y=B\right)\to seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)=seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
18	17 3	eqtr4di	$$⊢\left(x=A\wedge y=B\right)\to seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)=P$$
19	18	fveq1d	$$⊢\left(x=A\wedge y=B\right)\to seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k+1\right)=P\left(k+1\right)$$
20	19	eleq2d	$$⊢\left(x=A\wedge y=B\right)\to \left(k\in seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k+1\right)\leftrightarrow k\in P\left(k+1\right)\right)$$
21	20	rabbidv	$$⊢\left(x=A\wedge y=B\right)\to \left\{k\in {\mathbb{N}}_0|k\in seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k+1\right)\right\}=\left\{k\in {\mathbb{N}}_0|k\in P\left(k+1\right)\right\}$$
22		df-smu	$$⊢\mathrm{smul}=\left(x\in 𝒫{\mathbb{N}}_0,y\in 𝒫{\mathbb{N}}_0⟼\left\{k\in {\mathbb{N}}_0|k\in seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k+1\right)\right\}\right)$$
23	4	rabex	$$⊢\left\{k\in {\mathbb{N}}_0|k\in P\left(k+1\right)\right\}\in \mathrm{V}$$
24	21 22 23	ovmpoa	$$⊢\left(A\in 𝒫{\mathbb{N}}_0\wedge B\in 𝒫{\mathbb{N}}_0\right)\to A\mathrm{smul}B=\left\{k\in {\mathbb{N}}_0|k\in P\left(k+1\right)\right\}$$
25	6 8 24	syl2anc	$$⊢\phi \to A\mathrm{smul}B=\left\{k\in {\mathbb{N}}_0|k\in P\left(k+1\right)\right\}$$