Metamath Proof Explorer

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 ⊢ φ → A ⊆ ℕ 0
smup1.b ⊢ φ → B ⊆ ℕ 0
smup1.n ⊢ φ → N ∈ ℕ 0
Assertion smup1 ⊢ φ → A ∩ 0 ..^ N + 1 smul B = A ∩ 0 ..^ N smul B sadd n ∈ ℕ 0 | N ∈ A ∧ n − N ∈ B

Proof

Step Hyp Ref Expression
1 smup1.a ⊢ φ → A ⊆ ℕ 0
2 smup1.b ⊢ φ → B ⊆ ℕ 0
3 smup1.n ⊢ φ → N ∈ ℕ 0
4 eqid ⊢ seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
5 1 2 4 3 smupp1 ⊢ φ → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N sadd n ∈ ℕ 0 | N ∈ A ∧ n − N ∈ B
6 peano2nn0 ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ 0
7 3 6 syl ⊢ φ → N + 1 ∈ ℕ 0
8 1 2 4 7 smupval ⊢ φ → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1 = A ∩ 0 ..^ N + 1 smul B
9 1 2 4 3 smupval ⊢ φ → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N = A ∩ 0 ..^ N smul B
10 9 oveq1d ⊢ φ → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N sadd n ∈ ℕ 0 | N ∈ A ∧ n − N ∈ B = A ∩ 0 ..^ N smul B sadd n ∈ ℕ 0 | N ∈ A ∧ n − N ∈ B
11 5 8 10 3eqtr3d ⊢ φ → A ∩ 0 ..^ N + 1 smul B = A ∩ 0 ..^ N smul B sadd n ∈ ℕ 0 | N ∈ A ∧ n − N ∈ B