Metamath Proof Explorer

Theorem esumpfinval

Description: The value of the extended sum of a finite set of nonnegative finite terms. (Contributed by Thierry Arnoux, 28-Jun-2017) (Proof shortened by AV, 25-Jul-2019)

Ref Expression
Hypotheses esumpfinval.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
esumpfinval.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
Assertion esumpfinval ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 esumpfinval.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 esumpfinval.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
3 df-esum ⊢ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
4 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
5 xrge00 ⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
6 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
7 6 a1i ⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
8 xrge0tps ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp
9 8 a1i ⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp )
10 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
11 10 2 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
12 11 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
13 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
14 c0ex ⊢ 0 ∈ V
15 14 a1i ⊢ ( 𝜑 → 0 ∈ V )
16 13 1 2 15 fsuppmptdm ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) finSupp 0 )
17 xrge0topn ⊢ ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
18 17 eqcomi ⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
19 xrhaus ⊢ ( ordTop ‘ ≤ ) ∈ Haus
20 ovex ⊢ ( 0 [,] +∞ ) ∈ V
21 resthaus ⊢ ( ( ( ordTop ‘ ≤ ) ∈ Haus ∧ ( 0 [,] +∞ ) ∈ V ) → ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ Haus )
22 19 20 21 mp2an ⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ Haus
23 22 a1i ⊢ ( 𝜑 → ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ Haus )
24 4 5 7 9 1 12 16 18 23 haustsmsid ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = { ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) } )
25 24 unieqd ⊢ ( 𝜑 → ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ∪ { ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) } )
26 3 25 syl5eq ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ { ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) } )
27 ovex ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ V
28 27 unisn ⊢ ∪ { ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) } = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
29 26 28 eqtrdi ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
30 2 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,) +∞ ) )
31 esumpfinvallem ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
32 1 30 31 syl2anc ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
33 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
34 ax-resscn ⊢ ℝ ⊆ ℂ
35 33 34 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
36 35 2 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
37 1 36 gsumfsum ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 )
38 29 32 37 3eqtr2d ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐵 )