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