Metamath Proof Explorer

Theorem smufval

Description: The multiplication of two bit sequences as repeated sequence addition. (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses smuval.a ⊢ φ → A ⊆ ℕ 0
smuval.b ⊢ φ → B ⊆ ℕ 0
smuval.p ⊢ P = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
Assertion smufval ⊢ φ → A smul B = k ∈ ℕ 0 | k ∈ P ⁡ k + 1

Proof

Step Hyp Ref Expression
1 smuval.a ⊢ φ → A ⊆ ℕ 0
2 smuval.b ⊢ φ → B ⊆ ℕ 0
3 smuval.p ⊢ P = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
4 nn0ex ⊢ ℕ 0 ∈ V
5 4 elpw2 ⊢ A ∈ 𝒫 ℕ 0 ↔ A ⊆ ℕ 0
6 1 5 sylibr ⊢ φ → A ∈ 𝒫 ℕ 0
7 4 elpw2 ⊢ B ∈ 𝒫 ℕ 0 ↔ B ⊆ ℕ 0
8 2 7 sylibr ⊢ φ → B ∈ 𝒫 ℕ 0
9 simp1l ⊢ x = A ∧ y = B ∧ p ∈ 𝒫 ℕ 0 ∧ m ∈ ℕ 0 → x = A
10 9 eleq2d ⊢ x = A ∧ y = B ∧ p ∈ 𝒫 ℕ 0 ∧ m ∈ ℕ 0 → m ∈ x ↔ m ∈ A
11 simp1r ⊢ x = A ∧ y = B ∧ p ∈ 𝒫 ℕ 0 ∧ m ∈ ℕ 0 → y = B
12 11 eleq2d ⊢ x = A ∧ y = B ∧ p ∈ 𝒫 ℕ 0 ∧ m ∈ ℕ 0 → n − m ∈ y ↔ n − m ∈ B
13 10 12 anbi12d ⊢ x = A ∧ y = B ∧ p ∈ 𝒫 ℕ 0 ∧ m ∈ ℕ 0 → m ∈ x ∧ n − m ∈ y ↔ m ∈ A ∧ n − m ∈ B
14 13 rabbidv ⊢ x = A ∧ y = B ∧ p ∈ 𝒫 ℕ 0 ∧ m ∈ ℕ 0 → n ∈ ℕ 0 | m ∈ x ∧ n − m ∈ y = n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B
15 14 oveq2d ⊢ x = A ∧ y = B ∧ p ∈ 𝒫 ℕ 0 ∧ m ∈ ℕ 0 → p sadd n ∈ ℕ 0 | m ∈ x ∧ n − m ∈ y = p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B
16 15 mpoeq3dva ⊢ x = A ∧ y = B → p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ x ∧ n − m ∈ y = p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B
17 16 seqeq2d ⊢ x = A ∧ y = B → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ x ∧ n − m ∈ y 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
18 17 3 eqtr4di ⊢ x = A ∧ y = B → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ x ∧ n − m ∈ y n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 = P
19 18 fveq1d ⊢ x = A ∧ y = B → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ x ∧ n − m ∈ y n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k + 1 = P ⁡ k + 1
20 19 eleq2d ⊢ x = A ∧ y = B → k ∈ seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ x ∧ n − m ∈ y n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k + 1 ↔ k ∈ P ⁡ k + 1
21 20 rabbidv ⊢ x = A ∧ y = B → k ∈ ℕ 0 | k ∈ seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ x ∧ n − m ∈ y n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k + 1 = k ∈ ℕ 0 | k ∈ P ⁡ k + 1
22 df-smu ⊢ smul = x ∈ 𝒫 ℕ 0 , y ∈ 𝒫 ℕ 0 ⟼ k ∈ ℕ 0 | k ∈ seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ x ∧ n − m ∈ y n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k + 1
23 4 rabex ⊢ k ∈ ℕ 0 | k ∈ P ⁡ k + 1 ∈ V
24 21 22 23 ovmpoa ⊢ A ∈ 𝒫 ℕ 0 ∧ B ∈ 𝒫 ℕ 0 → A smul B = k ∈ ℕ 0 | k ∈ P ⁡ k + 1
25 6 8 24 syl2anc ⊢ φ → A smul B = k ∈ ℕ 0 | k ∈ P ⁡ k + 1