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	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
	smuval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
	smuval.p	⊢ 𝑃 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
Assertion	smufval	⊢ ( 𝜑 → ( 𝐴 smul 𝐵 ) = { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		smuval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2		smuval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3		smuval.p	⊢ 𝑃 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
4		nn0ex	⊢ ℕ0 ∈ V
5	4	elpw2	⊢ ( 𝐴 ∈ 𝒫 ℕ0 ↔ 𝐴 ⊆ ℕ0 )
6	1 5	sylibr	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 ℕ0 )
7	4	elpw2	⊢ ( 𝐵 ∈ 𝒫 ℕ0 ↔ 𝐵 ⊆ ℕ0 )
8	2 7	sylibr	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 ℕ0 )
9		simp1l	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑝 ∈ 𝒫 ℕ0 ∧ 𝑚 ∈ ℕ0 ) → 𝑥 = 𝐴 )
10	9	eleq2d	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑝 ∈ 𝒫 ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 ∈ 𝑥 ↔ 𝑚 ∈ 𝐴 ) )
11		simp1r	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑝 ∈ 𝒫 ℕ0 ∧ 𝑚 ∈ ℕ0 ) → 𝑦 = 𝐵 )
12	11	eleq2d	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑝 ∈ 𝒫 ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑛 − 𝑚 ) ∈ 𝑦 ↔ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) )
13	10 12	anbi12d	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑝 ∈ 𝒫 ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) ↔ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) ) )
14	13	rabbidv	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑝 ∈ 𝒫 ℕ0 ∧ 𝑚 ∈ ℕ0 ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } = { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } )
15	14	oveq2d	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑝 ∈ 𝒫 ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) = ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) )
16	15	mpoeq3dva	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) ) = ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) )
17	16	seqeq2d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) )
18	17 3	eqtr4di	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = 𝑃 )
19	18	fveq1d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
20	19	eleq2d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑘 ∈ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ↔ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
21	20	rabbidv	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) } = { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
22		df-smu	⊢ smul = ( 𝑥 ∈ 𝒫 ℕ0 , 𝑦 ∈ 𝒫 ℕ0 ↦ { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝑥 ∧ ( 𝑛 − 𝑚 ) ∈ 𝑦 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) } )
23	4	rabex	⊢ { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ V
24	21 22 23	ovmpoa	⊢ ( ( 𝐴 ∈ 𝒫 ℕ0 ∧ 𝐵 ∈ 𝒫 ℕ0 ) → ( 𝐴 smul 𝐵 ) = { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
25	6 8 24	syl2anc	⊢ ( 𝜑 → ( 𝐴 smul 𝐵 ) = { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )