Metamath Proof Explorer

Theorem smueqlem

Description: Any element of a sequence multiplication only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 20-Sep-2016)

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

Proof

Step Hyp Ref Expression
1 smueq.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2 smueq.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3 smueq.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 smueq.p ⊢ 𝑃 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
5 smueq.q ⊢ 𝑄 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
6 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ⊆ ℕ0 )
7 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ⊆ ℕ0 )
8 elfzouz ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
10 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
11 9 10 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
12 11 nn0zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ℤ )
13 12 peano2zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℤ )
14 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
15 14 nn0zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℤ )
16 elfzolt2 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 < 𝑁 )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 < 𝑁 )
18 nn0ltp1le ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑘 < 𝑁 ↔ ( 𝑘 + 1 ) ≤ 𝑁 ) )
19 11 14 18 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 < 𝑁 ↔ ( 𝑘 + 1 ) ≤ 𝑁 ) )
20 17 19 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ≤ 𝑁 )
21 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ↔ ( ( 𝑘 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) )
22 13 15 20 21 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
23 6 7 4 11 22 smuval2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑘 ∈ ( 𝑃 ‘ 𝑁 ) ) )
24 3 10 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
25 eluzfz2b ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) ↔ 𝑁 ∈ ( 0 ... 𝑁 ) )
26 24 25 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
27 fveq2 ⊢ ( 𝑥 = 0 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 0 ) )
28 27 ineq1d ⊢ ( 𝑥 = 0 → ( ( 𝑃 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑃 ‘ 0 ) ∩ ( 0 ..^ 𝑁 ) ) )
29 fveq2 ⊢ ( 𝑥 = 0 → ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ 0 ) )
30 29 ineq1d ⊢ ( 𝑥 = 0 → ( ( 𝑄 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 0 ) ∩ ( 0 ..^ 𝑁 ) ) )
31 28 30 eqeq12d ⊢ ( 𝑥 = 0 → ( ( ( 𝑃 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) ↔ ( ( 𝑃 ‘ 0 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 0 ) ∩ ( 0 ..^ 𝑁 ) ) ) )
32 31 imbi2d ⊢ ( 𝑥 = 0 → ( ( 𝜑 → ( ( 𝑃 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) ) ↔ ( 𝜑 → ( ( 𝑃 ‘ 0 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 0 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
33 fveq2 ⊢ ( 𝑥 = 𝑖 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑖 ) )
34 33 ineq1d ⊢ ( 𝑥 = 𝑖 → ( ( 𝑃 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑃 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) )
35 fveq2 ⊢ ( 𝑥 = 𝑖 → ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑖 ) )
36 35 ineq1d ⊢ ( 𝑥 = 𝑖 → ( ( 𝑄 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) )
37 34 36 eqeq12d ⊢ ( 𝑥 = 𝑖 → ( ( ( 𝑃 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) ↔ ( ( 𝑃 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) ) )
38 37 imbi2d ⊢ ( 𝑥 = 𝑖 → ( ( 𝜑 → ( ( 𝑃 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) ) ↔ ( 𝜑 → ( ( 𝑃 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
39 fveq2 ⊢ ( 𝑥 = ( 𝑖 + 1 ) → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
40 39 ineq1d ⊢ ( 𝑥 = ( 𝑖 + 1 ) → ( ( 𝑃 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) )
41 fveq2 ⊢ ( 𝑥 = ( 𝑖 + 1 ) → ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
42 41 ineq1d ⊢ ( 𝑥 = ( 𝑖 + 1 ) → ( ( 𝑄 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) )
43 40 42 eqeq12d ⊢ ( 𝑥 = ( 𝑖 + 1 ) → ( ( ( 𝑃 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) ↔ ( ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
44 43 imbi2d ⊢ ( 𝑥 = ( 𝑖 + 1 ) → ( ( 𝜑 → ( ( 𝑃 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) ) ↔ ( 𝜑 → ( ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
45 fveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) )
46 45 ineq1d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑃 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑃 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) )
47 fveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑁 ) )
48 47 ineq1d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑄 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) )
49 46 48 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( ( 𝑃 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) ↔ ( ( 𝑃 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) ) )
50 49 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( ( 𝑃 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑥 ) ∩ ( 0 ..^ 𝑁 ) ) ) ↔ ( 𝜑 → ( ( 𝑃 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
51 1 2 4 smup0 ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = ∅ )
52 inss1 ⊢ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ 𝐵
53 52 2 sstrid ⊢ ( 𝜑 → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
54 1 53 5 smup0 ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = ∅ )
55 51 54 eqtr4d ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = ( 𝑄 ‘ 0 ) )
56 55 ineq1d ⊢ ( 𝜑 → ( ( 𝑃 ‘ 0 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 0 ) ∩ ( 0 ..^ 𝑁 ) ) )
57 56 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 𝜑 → ( ( 𝑃 ‘ 0 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 0 ) ∩ ( 0 ..^ 𝑁 ) ) ) )
58 oveq1 ⊢ ( ( ( 𝑃 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑃 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ∩ ( 0 ..^ 𝑁 ) ) ) = ( ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ∩ ( 0 ..^ 𝑁 ) ) ) )
59 58 ineq1d ⊢ ( ( ( 𝑃 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝑃 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )
60 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ⊆ ℕ0 )
61 2 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ⊆ ℕ0 )
62 elfzonn0 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ℕ0 )
63 62 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ℕ0 )
64 60 61 4 63 smupp1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑃 ‘ 𝑖 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ) )
65 64 ineq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( 𝑃 ‘ 𝑖 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ) ∩ ( 0 ..^ 𝑁 ) ) )
66 1 2 4 smupf ⊢ ( 𝜑 → 𝑃 : ℕ0 ⟶ 𝒫 ℕ0 )
67 ffvelrn ⊢ ( ( 𝑃 : ℕ0 ⟶ 𝒫 ℕ0 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑃 ‘ 𝑖 ) ∈ 𝒫 ℕ0 )
68 66 62 67 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ 𝒫 ℕ0 )
69 68 elpwid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ⊆ ℕ0 )
70 ssrab2 ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ⊆ ℕ0
71 70 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ⊆ ℕ0 )
72 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
73 69 71 72 sadeq ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑃 ‘ 𝑖 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( ( 𝑃 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )
74 65 73 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( ( 𝑃 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )
75 53 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
76 60 75 5 63 smupp1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑄 ‘ 𝑖 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } ) )
77 76 ineq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( 𝑄 ‘ 𝑖 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } ) ∩ ( 0 ..^ 𝑁 ) ) )
78 1 53 5 smupf ⊢ ( 𝜑 → 𝑄 : ℕ0 ⟶ 𝒫 ℕ0 )
79 ffvelrn ⊢ ( ( 𝑄 : ℕ0 ⟶ 𝒫 ℕ0 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑄 ‘ 𝑖 ) ∈ 𝒫 ℕ0 )
80 78 62 79 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ 𝒫 ℕ0 )
81 80 elpwid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑄 ‘ 𝑖 ) ⊆ ℕ0 )
82 ssrab2 ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } ⊆ ℕ0
83 82 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } ⊆ ℕ0 )
84 81 83 72 sadeq ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )
85 elinel2 ⊢ ( 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ 𝑁 ) ) → 𝑛 ∈ ( 0 ..^ 𝑁 ) )
86 61 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ⊆ ℕ0 )
87 86 sseld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑛 − 𝑖 ) ∈ 𝐵 → ( 𝑛 − 𝑖 ) ∈ ℕ0 ) )
88 elfzo0 ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝑛 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑛 < 𝑁 ) )
89 88 simp2bi ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑁 ∈ ℕ )
90 89 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℕ )
91 elfzonn0 ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 ∈ ℕ0 )
92 91 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 ∈ ℕ0 )
93 92 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 ∈ ℝ )
94 63 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ℕ0 )
95 94 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ℝ )
96 93 95 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 − 𝑖 ) ∈ ℝ )
97 90 nnred ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℝ )
98 94 nn0ge0d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 0 ≤ 𝑖 )
99 93 95 subge02d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ≤ 𝑖 ↔ ( 𝑛 − 𝑖 ) ≤ 𝑛 ) )
100 98 99 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 − 𝑖 ) ≤ 𝑛 )
101 elfzolt2 ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 < 𝑁 )
102 101 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 < 𝑁 )
103 96 93 97 100 102 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 − 𝑖 ) < 𝑁 )
104 90 103 jca ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑁 ∈ ℕ ∧ ( 𝑛 − 𝑖 ) < 𝑁 ) )
105 elfzo0 ⊢ ( ( 𝑛 − 𝑖 ) ∈ ( 0 ..^ 𝑁 ) ↔ ( ( 𝑛 − 𝑖 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ ( 𝑛 − 𝑖 ) < 𝑁 ) )
106 3anass ⊢ ( ( ( 𝑛 − 𝑖 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ ( 𝑛 − 𝑖 ) < 𝑁 ) ↔ ( ( 𝑛 − 𝑖 ) ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝑛 − 𝑖 ) < 𝑁 ) ) )
107 105 106 bitri ⊢ ( ( 𝑛 − 𝑖 ) ∈ ( 0 ..^ 𝑁 ) ↔ ( ( 𝑛 − 𝑖 ) ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝑛 − 𝑖 ) < 𝑁 ) ) )
108 107 baib ⊢ ( ( 𝑛 − 𝑖 ) ∈ ℕ0 → ( ( 𝑛 − 𝑖 ) ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝑁 ∈ ℕ ∧ ( 𝑛 − 𝑖 ) < 𝑁 ) ) )
109 104 108 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑛 − 𝑖 ) ∈ ℕ0 → ( 𝑛 − 𝑖 ) ∈ ( 0 ..^ 𝑁 ) ) )
110 87 109 syld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑛 − 𝑖 ) ∈ 𝐵 → ( 𝑛 − 𝑖 ) ∈ ( 0 ..^ 𝑁 ) ) )
111 110 pm4.71rd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑛 − 𝑖 ) ∈ 𝐵 ↔ ( ( 𝑛 − 𝑖 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) ) )
112 ancom ⊢ ( ( ( 𝑛 − 𝑖 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) ↔ ( ( 𝑛 − 𝑖 ) ∈ 𝐵 ∧ ( 𝑛 − 𝑖 ) ∈ ( 0 ..^ 𝑁 ) ) )
113 elin ⊢ ( ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ↔ ( ( 𝑛 − 𝑖 ) ∈ 𝐵 ∧ ( 𝑛 − 𝑖 ) ∈ ( 0 ..^ 𝑁 ) ) )
114 112 113 bitr4i ⊢ ( ( ( 𝑛 − 𝑖 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) ↔ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) )
115 111 114 bitr2di ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ↔ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) )
116 115 anbi2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ↔ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) ) )
117 85 116 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ 𝑁 ) ) ) → ( ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ↔ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) ) )
118 117 rabbidva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → { 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ 𝑁 ) ) ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } = { 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ 𝑁 ) ) ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } )
119 inrab2 ⊢ ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } ∩ ( 0 ..^ 𝑁 ) ) = { 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ 𝑁 ) ) ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) }
120 inrab2 ⊢ ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ∩ ( 0 ..^ 𝑁 ) ) = { 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ 𝑁 ) ) ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) }
121 118 119 120 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } ∩ ( 0 ..^ 𝑁 ) ) = ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ∩ ( 0 ..^ 𝑁 ) ) )
122 121 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } ∩ ( 0 ..^ 𝑁 ) ) ) = ( ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ∩ ( 0 ..^ 𝑁 ) ) ) )
123 122 ineq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) } ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )
124 77 84 123 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )
125 74 124 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) ↔ ( ( ( ( 𝑃 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑖 ∈ 𝐴 ∧ ( 𝑛 − 𝑖 ) ∈ 𝐵 ) } ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
126 59 125 syl5ibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑃 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) → ( ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
127 126 expcom ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( 𝜑 → ( ( ( 𝑃 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) → ( ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
128 127 a2d ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝜑 → ( ( 𝑃 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑖 ) ∩ ( 0 ..^ 𝑁 ) ) ) → ( 𝜑 → ( ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
129 32 38 44 50 57 128 fzind2 ⊢ ( 𝑁 ∈ ( 0 ... 𝑁 ) → ( 𝜑 → ( ( 𝑃 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) ) )
130 26 129 mpcom ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) )
131 130 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑃 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) )
132 131 eleq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 ∈ ( ( 𝑃 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) ↔ 𝑘 ∈ ( ( 𝑄 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) ) )
133 elin ⊢ ( 𝑘 ∈ ( ( 𝑃 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) ↔ ( 𝑘 ∈ ( 𝑃 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) )
134 133 rbaib ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝑘 ∈ ( ( 𝑃 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) ↔ 𝑘 ∈ ( 𝑃 ‘ 𝑁 ) ) )
135 134 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 ∈ ( ( 𝑃 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) ↔ 𝑘 ∈ ( 𝑃 ‘ 𝑁 ) ) )
136 elin ⊢ ( 𝑘 ∈ ( ( 𝑄 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) ↔ ( 𝑘 ∈ ( 𝑄 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) )
137 136 rbaib ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝑘 ∈ ( ( 𝑄 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) ↔ 𝑘 ∈ ( 𝑄 ‘ 𝑁 ) ) )
138 137 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 ∈ ( ( 𝑄 ‘ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) ↔ 𝑘 ∈ ( 𝑄 ‘ 𝑁 ) ) )
139 132 135 138 3bitr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 ∈ ( 𝑃 ‘ 𝑁 ) ↔ 𝑘 ∈ ( 𝑄 ‘ 𝑁 ) ) )
140 53 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
141 6 140 5 14 smupval ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑄 ‘ 𝑁 ) = ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) )
142 141 eleq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 ∈ ( 𝑄 ‘ 𝑁 ) ↔ 𝑘 ∈ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) )
143 23 139 142 3bitrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑘 ∈ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) )
144 143 ex ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑘 ∈ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ) )
145 144 pm5.32rd ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ↔ ( 𝑘 ∈ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ) )
146 elin ⊢ ( 𝑘 ∈ ( ( 𝐴 smul 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ↔ ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) )
147 elin ⊢ ( 𝑘 ∈ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ↔ ( 𝑘 ∈ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) )
148 145 146 147 3bitr4g ⊢ ( 𝜑 → ( 𝑘 ∈ ( ( 𝐴 smul 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ↔ 𝑘 ∈ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
149 148 eqrdv ⊢ ( 𝜑 → ( ( 𝐴 smul 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) smul ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )