Theorem smupf

Description: The sequence of partial sums of the sequence multiplication. (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	smupf	⊢ ( 𝜑 → 𝑃 : ℕ0 ⟶ 𝒫 ℕ0 )

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		0nn0	⊢ 0 ∈ ℕ0
5		iftrue	⊢ ( 𝑛 = 0 → if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) = ∅ )
6		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) )
7		0ex	⊢ ∅ ∈ V
8	5 6 7	fvmpt	⊢ ( 0 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) = ∅ )
9	4 8	mp1i	⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) = ∅ )
10		0elpw	⊢ ∅ ∈ 𝒫 ℕ0
11	9 10	eqeltrdi	⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) ∈ 𝒫 ℕ0 )
12		df-ov	⊢ ( 𝑥 ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) 𝑦 ) = ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
13		elpwi	⊢ ( 𝑝 ∈ 𝒫 ℕ0 → 𝑝 ⊆ ℕ0 )
14	13	adantr	⊢ ( ( 𝑝 ∈ 𝒫 ℕ0 ∧ 𝑚 ∈ ℕ0 ) → 𝑝 ⊆ ℕ0 )
15		ssrab2	⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ⊆ ℕ0
16		sadcl	⊢ ( ( 𝑝 ⊆ ℕ0 ∧ { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ⊆ ℕ0 ) → ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ⊆ ℕ0 )
17	14 15 16	sylancl	⊢ ( ( 𝑝 ∈ 𝒫 ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ⊆ ℕ0 )
18		nn0ex	⊢ ℕ0 ∈ V
19	18	elpw2	⊢ ( ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ∈ 𝒫 ℕ0 ↔ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ⊆ ℕ0 )
20	17 19	sylibr	⊢ ( ( 𝑝 ∈ 𝒫 ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ∈ 𝒫 ℕ0 )
21	20	rgen2	⊢ ∀ 𝑝 ∈ 𝒫 ℕ0 ∀ 𝑚 ∈ ℕ0 ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ∈ 𝒫 ℕ0
22		eqid	⊢ ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) = ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) )
23	22	fmpo	⊢ ( ∀ 𝑝 ∈ 𝒫 ℕ0 ∀ 𝑚 ∈ ℕ0 ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ∈ 𝒫 ℕ0 ↔ ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) : ( 𝒫 ℕ0 × ℕ0 ) ⟶ 𝒫 ℕ0 )
24	21 23	mpbi	⊢ ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) : ( 𝒫 ℕ0 × ℕ0 ) ⟶ 𝒫 ℕ0
25	24 10	f0cli	⊢ ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝒫 ℕ0
26	12 25	eqeltri	⊢ ( 𝑥 ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) 𝑦 ) ∈ 𝒫 ℕ0
27	26	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 ℕ0 ∧ 𝑦 ∈ V ) ) → ( 𝑥 ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) 𝑦 ) ∈ 𝒫 ℕ0 )
28		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
29		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
30		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 𝑥 ) ∈ V )
31	11 27 28 29 30	seqf2	⊢ ( 𝜑 → seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) : ℕ0 ⟶ 𝒫 ℕ0 )
32	3	feq1i	⊢ ( 𝑃 : ℕ0 ⟶ 𝒫 ℕ0 ↔ seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) : ℕ0 ⟶ 𝒫 ℕ0 )
33	31 32	sylibr	⊢ ( 𝜑 → 𝑃 : ℕ0 ⟶ 𝒫 ℕ0 )