Metamath Proof Explorer

Theorem esumgsum

Description: A finite extended sum is the group sum over the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 24-Apr-2020)

Ref Expression
Hypotheses esumgsum.1 ⊢ Ⅎ k φ
esumgsum.2 ⊢ Ⅎ _ k A
esumgsum.3 ⊢ φ → A ∈ Fin
esumgsum.4 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
Assertion esumgsum ⊢ φ → ∑ * k ∈ A B = ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ A B

Proof

Step Hyp Ref Expression
1 esumgsum.1 ⊢ Ⅎ k φ
2 esumgsum.2 ⊢ Ⅎ _ k A
3 esumgsum.3 ⊢ φ → A ∈ Fin
4 esumgsum.4 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
5 xrge0base ⊢ 0 +∞ = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
6 xrge00 ⊢ 0 = 0 ℝ 𝑠 * ↾ 𝑠 0 +∞
7 xrge0cmn ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
8 7 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
9 xrge0tps ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp
10 9 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp
11 nfcv ⊢ Ⅎ _ k 0 +∞
12 eqid ⊢ k ∈ A ⟼ B = k ∈ A ⟼ B
13 1 2 11 4 12 fmptdF ⊢ φ → k ∈ A ⟼ B : A ⟶ 0 +∞
14 4 ex ⊢ φ → k ∈ A → B ∈ 0 +∞
15 1 14 ralrimi ⊢ φ → ∀ k ∈ A B ∈ 0 +∞
16 2 fnmptf ⊢ ∀ k ∈ A B ∈ 0 +∞ → k ∈ A ⟼ B Fn A
17 15 16 syl ⊢ φ → k ∈ A ⟼ B Fn A
18 0xr ⊢ 0 ∈ ℝ *
19 18 a1i ⊢ φ → 0 ∈ ℝ *
20 17 3 19 fndmfifsupp ⊢ φ → finSupp 0 ⁡ k ∈ A ⟼ B
21 5 6 8 10 3 13 20 tsmsid ⊢ φ → ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ A B ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B
22 1 2 3 4 21 esumid ⊢ φ → ∑ * k ∈ A B = ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ A B