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

Definition df-smu 15815
 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 15760 . 2 class smul
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cn0 11885 . . . 4 class 0
54cpw 4497 . . 3 class 𝒫 ℕ0
6 vk . . . . . 6 setvar 𝑘
76cv 1537 . . . . 5 class 𝑘
8 c1 10527 . . . . . . 7 class 1
9 caddc 10529 . . . . . . 7 class +
107, 8, 9co 7135 . . . . . 6 class (𝑘 + 1)
11 vp . . . . . . . 8 setvar 𝑝
12 vm . . . . . . . 8 setvar 𝑚
1311cv 1537 . . . . . . . . 9 class 𝑝
1412, 2wel 2112 . . . . . . . . . . 11 wff 𝑚𝑥
15 vn . . . . . . . . . . . . . 14 setvar 𝑛
1615cv 1537 . . . . . . . . . . . . 13 class 𝑛
1712cv 1537 . . . . . . . . . . . . 13 class 𝑚
18 cmin 10859 . . . . . . . . . . . . 13 class
1916, 17, 18co 7135 . . . . . . . . . . . 12 class (𝑛𝑚)
203cv 1537 . . . . . . . . . . . 12 class 𝑦
2119, 20wcel 2111 . . . . . . . . . . 11 wff (𝑛𝑚) ∈ 𝑦
2214, 21wa 399 . . . . . . . . . 10 wff (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)
2322, 15, 4crab 3110 . . . . . . . . 9 class {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)}
24 csad 15759 . . . . . . . . 9 class sadd
2513, 23, 24co 7135 . . . . . . . 8 class (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)})
2611, 12, 5, 4, 25cmpo 7137 . . . . . . 7 class (𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)}))
27 cc0 10526 . . . . . . . . . 10 class 0
2816, 27wceq 1538 . . . . . . . . 9 wff 𝑛 = 0
29 c0 4243 . . . . . . . . 9 class
3016, 8, 18co 7135 . . . . . . . . 9 class (𝑛 − 1)
3128, 29, 30cif 4425 . . . . . . . 8 class if(𝑛 = 0, ∅, (𝑛 − 1))
3215, 4, 31cmpt 5110 . . . . . . 7 class (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))
3326, 32, 27cseq 13364 . . . . . 6 class seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
3410, 33cfv 6324 . . . . 5 class (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))
357, 34wcel 2111 . . . 4 wff 𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))
3635, 6, 4crab 3110 . . 3 class {𝑘 ∈ ℕ0𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))}
372, 3, 5, 5, 36cmpo 7137 . 2 class (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚𝑥 ∧ (𝑛𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))})
381, 37wceq 1538 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  15816
 Copyright terms: Public domain W3C validator