Metamath Proof Explorer


Theorem esumel

Description: The extended sum is a limit point of the corresponding infinite group sum. (Contributed by Thierry Arnoux, 24-Mar-2017)

Ref Expression
Hypotheses esumel.1 𝑘 𝜑
esumel.2 𝑘 𝐴
esumel.3 ( 𝜑𝐴𝑉 )
esumel.4 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
Assertion esumel ( 𝜑 → Σ* 𝑘𝐴 𝐵 ∈ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 esumel.1 𝑘 𝜑
2 esumel.2 𝑘 𝐴
3 esumel.3 ( 𝜑𝐴𝑉 )
4 esumel.4 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
5 4 ex ( 𝜑 → ( 𝑘𝐴𝐵 ∈ ( 0 [,] +∞ ) ) )
6 1 5 ralrimi ( 𝜑 → ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
7 2 esumcl ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
8 3 6 7 syl2anc ( 𝜑 → Σ* 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
9 snidg ( Σ* 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) → Σ* 𝑘𝐴 𝐵 ∈ { Σ* 𝑘𝐴 𝐵 } )
10 8 9 syl ( 𝜑 → Σ* 𝑘𝐴 𝐵 ∈ { Σ* 𝑘𝐴 𝐵 } )
11 eqid ( ℝ*𝑠s ( 0 [,] +∞ ) ) = ( ℝ*𝑠s ( 0 [,] +∞ ) )
12 nfcv 𝑘 ( 0 [,] +∞ )
13 eqid ( 𝑘𝐴𝐵 ) = ( 𝑘𝐴𝐵 )
14 1 2 12 4 13 fmptdF ( 𝜑 → ( 𝑘𝐴𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
15 inss1 ( 𝒫 𝐴 ∩ Fin ) ⊆ 𝒫 𝐴
16 simpr ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) )
17 15 16 sselid ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ 𝒫 𝐴 )
18 17 elpwid ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥𝐴 )
19 nfcv 𝑘 𝑥
20 2 19 resmptf ( 𝑥𝐴 → ( ( 𝑘𝐴𝐵 ) ↾ 𝑥 ) = ( 𝑘𝑥𝐵 ) )
21 18 20 syl ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝑘𝐴𝐵 ) ↾ 𝑥 ) = ( 𝑘𝑥𝐵 ) )
22 21 eqcomd ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑘𝑥𝐵 ) = ( ( 𝑘𝐴𝐵 ) ↾ 𝑥 ) )
23 22 oveq2d ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( ( 𝑘𝐴𝐵 ) ↾ 𝑥 ) ) )
24 1 2 3 4 23 esumval ( 𝜑 → Σ* 𝑘𝐴 𝐵 = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( ( 𝑘𝐴𝐵 ) ↾ 𝑥 ) ) ) , ℝ* , < ) )
25 11 3 14 24 xrge0tsmsd ( 𝜑 → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) ) = { Σ* 𝑘𝐴 𝐵 } )
26 10 25 eleqtrrd ( 𝜑 → Σ* 𝑘𝐴 𝐵 ∈ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) ) )