sge0revalmpt

Description: Value of the sum of nonnegative extended reals, when all terms in the sum are reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0revalmpt.1	⊢ Ⅎ 𝑥 𝜑
	sge0revalmpt.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0revalmpt.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
Assertion	sge0revalmpt	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑥 ∈ 𝑦 𝐵 ) , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		sge0revalmpt.1	⊢ Ⅎ 𝑥 𝜑
2		sge0revalmpt.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0revalmpt.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
4		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	1 3 4	fmptdf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,) +∞ ) )
6	2 5	sge0reval	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) , ℝ^* , < ) )
7		fveq2	⊢ ( 𝑧 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
8		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
9		nfcv	⊢ Ⅎ 𝑥 𝑧
10	8 9	nffv	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 )
11		nfcv	⊢ Ⅎ 𝑧 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 )
12	7 10 11	cbvsum	⊢ Σ 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) = Σ 𝑥 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 )
13	12	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) = Σ 𝑥 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
14		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin )
15	1 14	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) )
16		elpwinss	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
17	16	adantr	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑥 ∈ 𝑦 ) → 𝑦 ⊆ 𝐴 )
18		simpr	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝑦 )
19	17 18	sseldd	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝐴 )
20	19	adantll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝐴 )
21		simpll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝜑 )
22	21 20 3	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
23	4	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
24	20 22 23	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
25	24	ex	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑥 ∈ 𝑦 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 ) )
26	15 25	ralrimi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∀ 𝑥 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
27		sumeq2	⊢ ( ∀ 𝑥 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 → Σ 𝑥 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = Σ 𝑥 ∈ 𝑦 𝐵 )
28	26 27	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑥 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = Σ 𝑥 ∈ 𝑦 𝐵 )
29	13 28	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) = Σ 𝑥 ∈ 𝑦 𝐵 )
30	29	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) = ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑥 ∈ 𝑦 𝐵 ) )
31	30	rneqd	⊢ ( 𝜑 → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) = ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑥 ∈ 𝑦 𝐵 ) )
32	31	supeq1d	⊢ ( 𝜑 → sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) , ℝ^* , < ) = sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑥 ∈ 𝑦 𝐵 ) , ℝ^* , < ) )
33	6 32	eqtrd	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑥 ∈ 𝑦 𝐵 ) , ℝ^* , < ) )

Metamath Proof Explorer

Theorem sge0revalmpt

Proof