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 ⊢ Ⅎ k φ
esumval.0 ⊢ Ⅎ _ k A
esumval.1 ⊢ φ → A ∈ V
esumval.2 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
esumval.3 ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ x B = C
Assertion esumval ⊢ φ → ∑ * k ∈ A B = sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ C ℝ * <

Proof

Step Hyp Ref Expression
1 esumval.p ⊢ Ⅎ k φ
2 esumval.0 ⊢ Ⅎ _ k A
3 esumval.1 ⊢ φ → A ∈ V
4 esumval.2 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
5 esumval.3 ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ x B = C
6 df-esum ⊢ ∑ * k ∈ A B = ⋃ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B
7 eqid ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞
8 nfcv ⊢ Ⅎ _ k 0 +∞
9 eqid ⊢ k ∈ A ⟼ B = k ∈ A ⟼ B
10 1 2 8 4 9 fmptdf2 ⊢ φ → k ∈ A ⟼ B : A ⟶ 0 +∞
11 inss1 ⊢ 𝒫 A ∩ Fin ⊆ 𝒫 A
12 11 sseli ⊢ x ∈ 𝒫 A ∩ Fin → x ∈ 𝒫 A
13 12 elpwid ⊢ x ∈ 𝒫 A ∩ Fin → x ⊆ A
14 13 adantl ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → x ⊆ A
15 nfcv ⊢ Ⅎ _ k x
16 2 15 resmptf ⊢ x ⊆ A → k ∈ A ⟼ B ↾ x = k ∈ x ⟼ B
17 14 16 syl ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → k ∈ A ⟼ B ↾ x = k ∈ x ⟼ B
18 17 oveq2d ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ A ⟼ B ↾ x = ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ x B
19 18 5 eqtr2d ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → C = ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ A ⟼ B ↾ x
20 19 mpteq2dva ⊢ φ → x ∈ 𝒫 A ∩ Fin ⟼ C = x ∈ 𝒫 A ∩ Fin ⟼ ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ A ⟼ B ↾ x
21 20 rneqd ⊢ φ → ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ C = ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ A ⟼ B ↾ x
22 21 supeq1d ⊢ φ → sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ C ℝ * < = sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ A ⟼ B ↾ x ℝ * <
23 7 3 10 22 xrge0tsmsd ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B = sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ C ℝ * <
24 23 unieqd ⊢ φ → ⋃ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B = ⋃ sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ C ℝ * <
25 6 24 eqtrid ⊢ φ → ∑ * k ∈ A B = ⋃ sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ C ℝ * <
26 xrltso ⊢ < Or ℝ *
27 26 supex ⊢ sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ C ℝ * < ∈ V
28 27 unisn ⊢ ⋃ sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ C ℝ * < = sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ C ℝ * <
29 25 28 eqtrdi ⊢ φ → ∑ * k ∈ A B = sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ C ℝ * <