Theorem sge0val

Description: The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	sge0val	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) → ( Σ^ ‘ 𝐹 ) = if ( +∞ ∈ ran 𝐹 , +∞ , sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) ) , ℝ* , < ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-sumge0	⊢ Σ^ = ( 𝑥 ∈ V ↦ if ( +∞ ∈ ran 𝑥 , +∞ , sup ( ran ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) , ℝ* , < ) ) )
2	1	a1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) → Σ^ = ( 𝑥 ∈ V ↦ if ( +∞ ∈ ran 𝑥 , +∞ , sup ( ran ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) , ℝ* , < ) ) ) )
3		rneq	⊢ ( 𝑥 = 𝐹 → ran 𝑥 = ran 𝐹 )
4	3	eleq2d	⊢ ( 𝑥 = 𝐹 → ( +∞ ∈ ran 𝑥 ↔ +∞ ∈ ran 𝐹 ) )
5	4	adantl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑥 = 𝐹 ) → ( +∞ ∈ ran 𝑥 ↔ +∞ ∈ ran 𝐹 ) )
6		dmeq	⊢ ( 𝑥 = 𝐹 → dom 𝑥 = dom 𝐹 )
7	6	adantl	⊢ ( ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = 𝐹 ) → dom 𝑥 = dom 𝐹 )
8		fdm	⊢ ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) → dom 𝐹 = 𝑋 )
9	8	adantr	⊢ ( ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = 𝐹 ) → dom 𝐹 = 𝑋 )
10	7 9	eqtrd	⊢ ( ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = 𝐹 ) → dom 𝑥 = 𝑋 )
11	10	pweqd	⊢ ( ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = 𝐹 ) → 𝒫 dom 𝑥 = 𝒫 𝑋 )
12	11	ineq1d	⊢ ( ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = 𝐹 ) → ( 𝒫 dom 𝑥 ∩ Fin ) = ( 𝒫 𝑋 ∩ Fin ) )
13	12	mpteq1d	⊢ ( ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = 𝐹 ) → ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) = ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) )
14	13	adantll	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑥 = 𝐹 ) → ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) = ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) )
15		fveq1	⊢ ( 𝑥 = 𝐹 → ( 𝑥 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
16	15	sumeq2sdv	⊢ ( 𝑥 = 𝐹 → Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) = Σ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) )
17	16	mpteq2dv	⊢ ( 𝑥 = 𝐹 → ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) = ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) ) )
18	17	adantl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑥 = 𝐹 ) → ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) = ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) ) )
19	14 18	eqtrd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑥 = 𝐹 ) → ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) = ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) ) )
20	19	rneqd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑥 = 𝐹 ) → ran ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) = ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) ) )
21	20	supeq1d	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑥 = 𝐹 ) → sup ( ran ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) , ℝ* , < ) = sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) ) , ℝ* , < ) )
22	5 21	ifbieq2d	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑥 = 𝐹 ) → if ( +∞ ∈ ran 𝑥 , +∞ , sup ( ran ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) , ℝ* , < ) ) = if ( +∞ ∈ ran 𝐹 , +∞ , sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) ) , ℝ* , < ) ) )
23		simpr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
24		simpl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) → 𝑋 ∈ 𝑉 )
25	23 24	fexd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) → 𝐹 ∈ V )
26		pnfxr	⊢ +∞ ∈ ℝ*
27	26	a1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) → +∞ ∈ ℝ* )
28		xrltso	⊢ < Or ℝ*
29	28	supex	⊢ sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) ) , ℝ* , < ) ∈ V
30	29	a1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) → sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) ) , ℝ* , < ) ∈ V )
31	27 30	ifexd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) → if ( +∞ ∈ ran 𝐹 , +∞ , sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) ) , ℝ* , < ) ) ∈ V )
32	2 22 25 31	fvmptd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) → ( Σ^ ‘ 𝐹 ) = if ( +∞ ∈ ran 𝐹 , +∞ , sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝐹 ‘ 𝑤 ) ) , ℝ* , < ) ) )