MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-smu Structured version   Visualization version   GIF version

Definition df-smu 15192
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
StepHypRef Expression
1 csmu 15137 . 2 class smul
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cn0 11289 . . . 4 class 0
54cpw 4156 . . 3 class 𝒫 ℕ0
6 vk . . . . . 6 setvar 𝑘
76cv 1481 . . . . 5 class 𝑘
8 c1 9934 . . . . . . 7 class 1
9 caddc 9936 . . . . . . 7 class +
107, 8, 9co 6647 . . . . . 6 class (𝑘 + 1)
11 vp . . . . . . . 8 setvar 𝑝
12 vm . . . . . . . 8 setvar 𝑚
1311cv 1481 . . . . . . . . 9 class 𝑝
1412, 2wel 1990 . . . . . . . . . . 11 wff 𝑚𝑥
15 vn . . . . . . . . . . . . . 14 setvar 𝑛
1615cv 1481 . . . . . . . . . . . . 13 class 𝑛
1712cv 1481 . . . . . . . . . . . . 13 class 𝑚
18 cmin 10263 . . . . . . . . . . . . 13 class
1916, 17, 18co 6647 . . . . . . . . . . . 12 class (𝑛𝑚)
203cv 1481 . . . . . . . . . . . 12 class 𝑦
2119, 20wcel 1989 . . . . . . . . . . 11 wff (𝑛𝑚) ∈ 𝑦
2214, 21wa 384 . . . . . . . . . 10 wff (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)
2322, 15, 4crab 2915 . . . . . . . . 9 class {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)}
24 csad 15136 . . . . . . . . 9 class sadd
2513, 23, 24co 6647 . . . . . . . 8 class (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)})
2611, 12, 5, 4, 25cmpt2 6649 . . . . . . 7 class (𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)}))
27 cc0 9933 . . . . . . . . . 10 class 0
2816, 27wceq 1482 . . . . . . . . 9 wff 𝑛 = 0
29 c0 3913 . . . . . . . . 9 class
3016, 8, 18co 6647 . . . . . . . . 9 class (𝑛 − 1)
3128, 29, 30cif 4084 . . . . . . . 8 class if(𝑛 = 0, ∅, (𝑛 − 1))
3215, 4, 31cmpt 4727 . . . . . . 7 class (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))
3326, 32, 27cseq 12796 . . . . . 6 class seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
3410, 33cfv 5886 . . . . 5 class (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))
357, 34wcel 1989 . . . 4 wff 𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))
3635, 6, 4crab 2915 . . 3 class {𝑘 ∈ ℕ0𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))}
372, 3, 5, 5, 36cmpt2 6649 . 2 class (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))})
381, 37wceq 1482 1 wff smul = (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))})
Colors of variables: wff setvar class
This definition is referenced by:  smufval  15193
  Copyright terms: Public domain W3C validator