Theorem smueq

Description: Any element of a sequence multiplication only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 20-Sep-2016)

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

Proof

Step	Hyp	Ref	Expression
1		smueq.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
2		smueq.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
3		smueq.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		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 \left(B\cap \left(0..^N\right)\right)\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 \left(B\cap \left(0..^N\right)\right)\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
6	1 2 3 4 5	smueqlem	$$⊢\phi \to \left(A\mathrm{smul}B\right)\cap \left(0..^N\right)=\left(\left(A\cap \left(0..^N\right)\right)\mathrm{smul}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)$$