Metamath Proof Explorer

Theorem esumval

Description: Develop the value of the extended sum. (Contributed by Thierry Arnoux, 4-Jan-2017)

Ref Expression
Hypotheses esumval.p ⊢ Ⅎ 𝑘 𝜑
esumval.0 ⊢ Ⅎ 𝑘 𝐴
esumval.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esumval.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
esumval.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) = 𝐶 )
Assertion esumval ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 𝐶 ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 esumval.p ⊢ Ⅎ 𝑘 𝜑
2 esumval.0 ⊢ Ⅎ 𝑘 𝐴
3 esumval.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 esumval.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
5 esumval.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) = 𝐶 )
6 df-esum ⊢ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
7 eqid ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
8 nfcv ⊢ Ⅎ 𝑘 ( 0 [,] +∞ )
9 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
10 1 2 8 4 9 fmptdF ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
11 inss1 ⊢ ( 𝒫 𝐴 ∩ Fin ) ⊆ 𝒫 𝐴
12 11 sseli ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ∈ 𝒫 𝐴 )
13 12 elpwid ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ⊆ 𝐴 )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ⊆ 𝐴 )
15 nfcv ⊢ Ⅎ 𝑘 𝑥
16 2 15 resmptf ⊢ ( 𝑥 ⊆ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) = ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) )
17 14 16 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) = ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) )
18 17 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) )
19 18 5 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐶 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) )
20 19 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 𝐶 ) = ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) ) )
21 20 rneqd ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 𝐶 ) = ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) ) )
22 21 supeq1d ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 𝐶 ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) ) , ℝ* , < ) )
23 7 3 10 22 xrge0tsmsd ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = { sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 𝐶 ) , ℝ* , < ) } )
24 23 unieqd ⊢ ( 𝜑 → ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ∪ { sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 𝐶 ) , ℝ* , < ) } )
25 6 24 syl5eq ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ { sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 𝐶 ) , ℝ* , < ) } )
26 xrltso ⊢ < Or ℝ*
27 26 supex ⊢ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 𝐶 ) , ℝ* , < ) ∈ V
28 27 unisn ⊢ ∪ { sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 𝐶 ) , ℝ* , < ) } = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 𝐶 ) , ℝ* , < )
29 25 28 eqtrdi ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 𝐶 ) , ℝ* , < ) )