Step | Hyp | Ref
| Expression |
1 | | df-sumge0 42652 |
. . 3
⊢
Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran
𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, <
))) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) →
Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran
𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, <
)))) |
3 | | rneq 5809 |
. . . . 5
⊢ (𝑥 = 𝐹 → ran 𝑥 = ran 𝐹) |
4 | 3 | eleq2d 2901 |
. . . 4
⊢ (𝑥 = 𝐹 → (+∞ ∈ ran 𝑥 ↔ +∞ ∈ ran
𝐹)) |
5 | 4 | adantl 484 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → (+∞ ∈ ran 𝑥 ↔ +∞ ∈ ran
𝐹)) |
6 | | dmeq 5775 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐹 → dom 𝑥 = dom 𝐹) |
7 | 6 | adantl 484 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 = 𝐹) → dom 𝑥 = dom 𝐹) |
8 | | fdm 6525 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋⟶(0[,]+∞) → dom 𝐹 = 𝑋) |
9 | 8 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 = 𝐹) → dom 𝐹 = 𝑋) |
10 | 7, 9 | eqtrd 2859 |
. . . . . . . . . 10
⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 = 𝐹) → dom 𝑥 = 𝑋) |
11 | 10 | pweqd 4561 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 = 𝐹) → 𝒫 dom 𝑥 = 𝒫 𝑋) |
12 | 11 | ineq1d 4191 |
. . . . . . . 8
⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 = 𝐹) → (𝒫 dom 𝑥 ∩ Fin) = (𝒫 𝑋 ∩ Fin)) |
13 | 12 | mpteq1d 5158 |
. . . . . . 7
⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 = 𝐹) → (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) = (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤))) |
14 | 13 | adantll 712 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) = (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤))) |
15 | | fveq1 6672 |
. . . . . . . . 9
⊢ (𝑥 = 𝐹 → (𝑥‘𝑤) = (𝐹‘𝑤)) |
16 | 15 | sumeq2sdv 15064 |
. . . . . . . 8
⊢ (𝑥 = 𝐹 → Σ𝑤 ∈ 𝑦 (𝑥‘𝑤) = Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)) |
17 | 16 | mpteq2dv 5165 |
. . . . . . 7
⊢ (𝑥 = 𝐹 → (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) = (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤))) |
18 | 17 | adantl 484 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) = (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤))) |
19 | 14, 18 | eqtrd 2859 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) = (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤))) |
20 | 19 | rneqd 5811 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) = ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤))) |
21 | 20 | supeq1d 8913 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < ) = sup(ran
(𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, <
)) |
22 | 5, 21 | ifbieq2d 4495 |
. 2
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < )) =
if(+∞ ∈ ran 𝐹,
+∞, sup(ran (𝑦 ∈
(𝒫 𝑋 ∩ Fin)
↦ Σ𝑤 ∈
𝑦 (𝐹‘𝑤)), ℝ*, <
))) |
23 | | simpr 487 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → 𝐹:𝑋⟶(0[,]+∞)) |
24 | | simpl 485 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → 𝑋 ∈ 𝑉) |
25 | | fex 6992 |
. . 3
⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑋 ∈ 𝑉) → 𝐹 ∈ V) |
26 | 23, 24, 25 | syl2anc 586 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → 𝐹 ∈ V) |
27 | | pnfxr 10698 |
. . . 4
⊢ +∞
∈ ℝ* |
28 | 27 | a1i 11 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → +∞
∈ ℝ*) |
29 | | xrltso 12537 |
. . . . 5
⊢ < Or
ℝ* |
30 | 29 | supex 8930 |
. . . 4
⊢ sup(ran
(𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < ) ∈
V |
31 | 30 | a1i 11 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → sup(ran
(𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < ) ∈
V) |
32 | | ifexg 4517 |
. . 3
⊢
((+∞ ∈ ℝ* ∧ sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < ) ∈ V)
→ if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < )) ∈
V) |
33 | 28, 31, 32 | syl2anc 586 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → if(+∞
∈ ran 𝐹, +∞,
sup(ran (𝑦 ∈
(𝒫 𝑋 ∩ Fin)
↦ Σ𝑤 ∈
𝑦 (𝐹‘𝑤)), ℝ*, < )) ∈
V) |
34 | 2, 22, 26, 33 | fvmptd 6778 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) →
(Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, <
))) |