Theorem smup1

Description: Rewrite smupp1 using only smul instead of the internal recursive function P . (Contributed by Mario Carneiro, 20-Sep-2016)

	Ref	Expression
Hypotheses	smup1.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
	smup1.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
	smup1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	smup1	$$⊢\phi \to \left(A\cap \left(0..^N+1\right)\right)\mathrm{smul}B=\left(\left(A\cap \left(0..^N\right)\right)\mathrm{smul}B\right)\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(N\in A\wedge n-N\in B\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		smup1.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
2		smup1.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
3		smup1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
4		eqid	$$⊢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)=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)$$
5	1 2 4 3	smupp1	$$⊢\phi \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 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)\left(N+1\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)\left(N\right)\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(N\in A\wedge n-N\in B\right)\right\}$$
6		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
7	3 6	syl	$$⊢\phi \to N+1\in {\mathbb{N}}_0$$
8	1 2 4 7	smupval	$$⊢\phi \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 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)\left(N+1\right)=\left(A\cap \left(0..^N+1\right)\right)\mathrm{smul}B$$
9	1 2 4 3	smupval	$$⊢\phi \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 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)\left(N\right)=\left(A\cap \left(0..^N\right)\right)\mathrm{smul}B$$
10	9	oveq1d	$$⊢\phi \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 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)\left(N\right)\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(N\in A\wedge n-N\in B\right)\right\}=\left(\left(A\cap \left(0..^N\right)\right)\mathrm{smul}B\right)\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(N\in A\wedge n-N\in B\right)\right\}$$
11	5 8 10	3eqtr3d	$$⊢\phi \to \left(A\cap \left(0..^N+1\right)\right)\mathrm{smul}B=\left(\left(A\cap \left(0..^N\right)\right)\mathrm{smul}B\right)\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(N\in A\wedge n-N\in B\right)\right\}$$