Definition df-smu

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csmu	⊢ smul
1		vx	⊢ 𝑥
2		cn0	⊢ ℕ0
3	2	cpw	⊢ 𝒫 ℕ0
4		vy	⊢ 𝑦
5		vk	⊢ 𝑘
6	5	cv	⊢ 𝑘
7		cc0	⊢ 0
8		vp	⊢ 𝑝
9		vm	⊢ 𝑚
10	8	cv	⊢ 𝑝
11		csad	⊢ sadd
12		vn	⊢ 𝑛
13	9	cv	⊢ 𝑚
14	1	cv	⊢ 𝑥
15	13 14	wcel	⊢ 𝑚 ∈ 𝑥
16	12	cv	⊢ 𝑛
17		cmin	⊢ −
18	16 13 17	co	⊢ ( 𝑛 − 𝑚 )
19	4	cv	⊢ 𝑦
20	18 19	wcel	⊢ ( 𝑛 − 𝑚 ) ∈ 𝑦
21	15 20	wa	⊢ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 )
22	21 12 2	crab	⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) }
23	10 22 11	co	⊢ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } )
24	8 9 3 2 23	cmpo	⊢ ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) )
25	16 7	wceq	⊢ 𝑛 = 0
26		c0	⊢ ∅
27		c1	⊢ 1
28	16 27 17	co	⊢ ( 𝑛 − 1 )
29	25 26 28	cif	⊢ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) )
30	12 2 29	cmpt	⊢ ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) )
31	24 30 7	cseq	⊢ seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
32		caddc	⊢ +
33	6 27 32	co	⊢ ( 𝑘 + 1 )
34	33 31	cfv	⊢ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) )
35	6 34	wcel	⊢ 𝑘 ∈ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) )
36	35 5 2	crab	⊢ { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) }
37	1 4 3 3 36	cmpo	⊢ ( 𝑥 ∈ 𝒫 ℕ0 , 𝑦 ∈ 𝒫 ℕ0 ↦ { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) } )
38	0 37	wceq	⊢ smul = ( 𝑥 ∈ 𝒫 ℕ0 , 𝑦 ∈ 𝒫 ℕ0 ↦ { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) } )