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	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
	smup1.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
	smup1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	smup1	⊢ ( 𝜑 → ( ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) smul 𝐵 ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul 𝐵 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		smup1.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2		smup1.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3		smup1.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	1 2 4 3	smupp1	⊢ ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) } ) )
6		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
7	3 6	syl	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
8	1 2 4 7	smupval	⊢ ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑁 + 1 ) ) = ( ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) smul 𝐵 ) )
9	1 2 4 3	smupval	⊢ ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) = ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul 𝐵 ) )
10	9	oveq1d	⊢ ( 𝜑 → ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) } ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul 𝐵 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) } ) )
11	5 8 10	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) smul 𝐵 ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul 𝐵 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) } ) )