Definition df-smu 15036

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

Assertion

Ref	Expression
df-smu	⊢ smul = (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ 𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝑥 ∧ (𝑛 − 𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))})

Distinct variable group:   𝑘,𝑚,𝑛,𝑝,𝑥,𝑦

Detailed syntax breakdown of Definition df-smu

Step	Hyp	Ref	Expression
1		csmu 14981	. 2 class smul
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cn0 11169	. . . 4 class ℕ0
5	4	cpw 4108	. . 3 class 𝒫 ℕ0
6		vk	. . . . . 6 setvar 𝑘
7	6	cv 1474	. . . . 5 class 𝑘
8		c1 9816	. . . . . . 7 class 1
9		caddc 9818	. . . . . . 7 class +
10	7, 8, 9	co 6549	. . . . . 6 class (𝑘 + 1)
11		vp	. . . . . . . 8 setvar 𝑝
12		vm	. . . . . . . 8 setvar 𝑚
13	11	cv 1474	. . . . . . . . 9 class 𝑝
14	12, 2	wel 1978	. . . . . . . . . . 11 wff 𝑚 ∈ 𝑥
15		vn	. . . . . . . . . . . . . 14 setvar 𝑛
16	15	cv 1474	. . . . . . . . . . . . 13 class 𝑛
17	12	cv 1474	. . . . . . . . . . . . 13 class 𝑚
18		cmin 10145	. . . . . . . . . . . . 13 class −
19	16, 17, 18	co 6549	. . . . . . . . . . . 12 class (𝑛 − 𝑚)
20	3	cv 1474	. . . . . . . . . . . 12 class 𝑦
21	19, 20	wcel 1977	. . . . . . . . . . 11 wff (𝑛 − 𝑚) ∈ 𝑦
22	14, 21	wa 383	. . . . . . . . . 10 wff (𝑚 ∈ 𝑥 ∧ (𝑛 − 𝑚) ∈ 𝑦)
23	22, 15, 4	crab 2900	. . . . . . . . 9 class {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝑥 ∧ (𝑛 − 𝑚) ∈ 𝑦)}
24		csad 14980	. . . . . . . . 9 class sadd
25	13, 23, 24	co 6549	. . . . . . . 8 class (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝑥 ∧ (𝑛 − 𝑚) ∈ 𝑦)})
26	11, 12, 5, 4, 25	cmpt2 6551	. . . . . . 7 class (𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝑥 ∧ (𝑛 − 𝑚) ∈ 𝑦)}))
27		cc0 9815	. . . . . . . . . 10 class 0
28	16, 27	wceq 1475	. . . . . . . . 9 wff 𝑛 = 0
29		c0 3874	. . . . . . . . 9 class ∅
30	16, 8, 18	co 6549	. . . . . . . . 9 class (𝑛 − 1)
31	28, 29, 30	cif 4036	. . . . . . . 8 class if(𝑛 = 0, ∅, (𝑛 − 1))
32	15, 4, 31	cmpt 4643	. . . . . . 7 class (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))
33	26, 32, 27	cseq 12663	. . . . . 6 class seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝑥 ∧ (𝑛 − 𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
34	10, 33	cfv 5804	. . . . 5 class (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝑥 ∧ (𝑛 − 𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))
35	7, 34	wcel 1977	. . . 4 wff 𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝑥 ∧ (𝑛 − 𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))
36	35, 6, 4	crab 2900	. . 3 class {𝑘 ∈ ℕ0 ∣ 𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝑥 ∧ (𝑛 − 𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))}
37	2, 3, 5, 5, 36	cmpt2 6551	. 2 class (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ 𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝑥 ∧ (𝑛 − 𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))})
38	1, 37	wceq 1475	1 wff smul = (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ 𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝑥 ∧ (𝑛 − 𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))})

This definition is referenced by:  smufval  15037