Metamath Proof Explorer

Theorem esumss

Description: Change the index set to a subset by adding zeroes. (Contributed by Thierry Arnoux, 19-Jun-2017)

Ref Expression
Hypotheses esumss.p ⊢ Ⅎ k φ
esumss.a ⊢ Ⅎ _ k A
esumss.b ⊢ Ⅎ _ k B
esumss.1 ⊢ φ → A ⊆ B
esumss.2 ⊢ φ → B ∈ V
esumss.3 ⊢ φ ∧ k ∈ B → C ∈ 0 +∞
esumss.4 ⊢ φ ∧ k ∈ B ∖ A → C = 0
Assertion esumss ⊢ φ → ∑ * k ∈ A C = ∑ * k ∈ B C

Proof

Step Hyp Ref Expression
1 esumss.p ⊢ Ⅎ k φ
2 esumss.a ⊢ Ⅎ _ k A
3 esumss.b ⊢ Ⅎ _ k B
4 esumss.1 ⊢ φ → A ⊆ B
5 esumss.2 ⊢ φ → B ∈ V
6 esumss.3 ⊢ φ ∧ k ∈ B → C ∈ 0 +∞
7 esumss.4 ⊢ φ ∧ k ∈ B ∖ A → C = 0
8 3 2 resmptf ⊢ A ⊆ B → k ∈ B ⟼ C ↾ A = k ∈ A ⟼ C
9 4 8 syl ⊢ φ → k ∈ B ⟼ C ↾ A = k ∈ A ⟼ C
10 9 oveq2d ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ B ⟼ C ↾ A = ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ C
11 xrge0base ⊢ 0 +∞ = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
12 xrge00 ⊢ 0 = 0 ℝ 𝑠 * ↾ 𝑠 0 +∞
13 xrge0cmn ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
14 13 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
15 xrge0tps ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp
16 15 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp
17 nfcv ⊢ Ⅎ _ k 0 +∞
18 eqid ⊢ k ∈ B ⟼ C = k ∈ B ⟼ C
19 1 3 17 6 18 fmptdf2 ⊢ φ → k ∈ B ⟼ C : B ⟶ 0 +∞
20 1 3 2 7 5 suppss2f ⊢ φ → k ∈ B ⟼ C supp 0 ⊆ A
21 11 12 14 16 5 19 20 tsmsres ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ B ⟼ C ↾ A = ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ B ⟼ C
22 10 21 eqtr3d ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ C = ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ B ⟼ C
23 22 unieqd ⊢ φ → ⋃ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ C = ⋃ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ B ⟼ C
24 df-esum ⊢ ∑ * k ∈ A C = ⋃ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ C
25 df-esum ⊢ ∑ * k ∈ B C = ⋃ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ B ⟼ C
26 23 24 25 3eqtr4g ⊢ φ → ∑ * k ∈ A C = ∑ * k ∈ B C