Metamath Proof Explorer

Theorem smupval

Description: Rewrite the elements of the partial sum sequence in terms of sequence multiplication. (Contributed by Mario Carneiro, 20-Sep-2016)

Ref Expression
Hypotheses smupval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
smupval.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
smupval.p ⊢ 𝑃 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
smupval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion smupval ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul 𝐵 ) )

Proof

Step Hyp Ref Expression
1 smupval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2 smupval.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3 smupval.p ⊢ 𝑃 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
4 smupval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
6 4 5 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
7 eluzfz2b ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) ↔ 𝑁 ∈ ( 0 ... 𝑁 ) )
8 6 7 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
9 fveq2 ⊢ ( 𝑥 = 0 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 0 ) )
10 fveq2 ⊢ ( 𝑥 = 0 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 ) )
11 9 10 eqeq12d ⊢ ( 𝑥 = 0 → ( ( 𝑃 ‘ 𝑥 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) ↔ ( 𝑃 ‘ 0 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 ) ) )
12 11 imbi2d ⊢ ( 𝑥 = 0 → ( ( 𝜑 → ( 𝑃 ‘ 𝑥 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) ) ↔ ( 𝜑 → ( 𝑃 ‘ 0 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 ) ) ) )
13 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑘 ) )
14 fveq2 ⊢ ( 𝑥 = 𝑘 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) )
15 13 14 eqeq12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑃 ‘ 𝑥 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) ↔ ( 𝑃 ‘ 𝑘 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) )
16 15 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 → ( 𝑃 ‘ 𝑥 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) ) ↔ ( 𝜑 → ( 𝑃 ‘ 𝑘 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) ) )
17 fveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
18 fveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) )
19 17 18 eqeq12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝑃 ‘ 𝑥 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) ↔ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
20 19 imbi2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( 𝑃 ‘ 𝑥 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) ) ↔ ( 𝜑 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) ) )
21 fveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) )
22 fveq2 ⊢ ( 𝑥 = 𝑁 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) )
23 21 22 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑃 ‘ 𝑥 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) ↔ ( 𝑃 ‘ 𝑁 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) ) )
24 23 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝑃 ‘ 𝑥 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) ) ↔ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) ) ) )
25 1 2 3 smup0 ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = ∅ )
26 inss1 ⊢ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ 𝐴
27 26 1 sstrid ⊢ ( 𝜑 → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
28 eqid ⊢ seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
29 27 2 28 smup0 ⊢ ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 ) = ∅ )
30 25 29 eqtr4d ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 ) )
31 30 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 𝜑 → ( 𝑃 ‘ 0 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 ) ) )
32 oveq1 ⊢ ( ( 𝑃 ‘ 𝑘 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) → ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) = ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) )
33 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ⊆ ℕ0 )
34 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ⊆ ℕ0 )
35 elfzouz ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
36 35 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
37 36 5 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
38 33 34 3 37 smupp1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) )
39 27 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
40 39 34 28 37 smupp1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) )
41 elin ⊢ ( 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ↔ ( 𝑘 ∈ 𝐴 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) )
42 41 rbaib ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ↔ 𝑘 ∈ 𝐴 ) )
43 42 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ↔ 𝑘 ∈ 𝐴 ) )
44 43 anbi1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) ↔ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) ) )
45 44 rabbidv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } = { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } )
46 45 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) = ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) )
47 40 46 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) )
48 38 47 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ↔ ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) = ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) ) )
49 32 48 syl5ibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑃 ‘ 𝑘 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
50 49 expcom ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝜑 → ( ( 𝑃 ‘ 𝑘 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) ) )
51 50 a2d ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝜑 → ( 𝑃 ‘ 𝑘 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) → ( 𝜑 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) ) )
52 12 16 20 24 31 51 fzind2 ⊢ ( 𝑁 ∈ ( 0 ... 𝑁 ) → ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) ) )
53 8 52 mpcom ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) )
54 inss2 ⊢ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
55 54 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) )
56 4 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
57 uzid ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
58 56 57 syl ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
59 27 2 28 4 55 58 smupvallem ⊢ ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) = ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul 𝐵 ) )
60 53 59 eqtrd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul 𝐵 ) )