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	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
	smueq.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
	smueq.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	smueq	⊢ ( 𝜑 → ( ( 𝐴 smul 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		smueq.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2		smueq.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3		smueq.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4		eqid	⊢ seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
5		eqid	⊢ seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
6	1 2 3 4 5	smueqlem	⊢ ( 𝜑 → ( ( 𝐴 smul 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )