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		nfcv	⊢ Ⅎ 𝑥 𝑦
9		nfcv	⊢ Ⅎ 𝑧 𝑦
10		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
11		nfcv	⊢ Ⅎ 𝑥 𝑧
12	10 11	nffv	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 )
13		nfcv	⊢ Ⅎ 𝑧 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 )
14	7 8 9 12 13	cbvsum	⊢ Σ 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) = Σ 𝑥 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 )
15	14	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) = Σ 𝑥 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
16		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin )
17	1 16	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) )
18		elpwinss	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
19	18	adantr	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑥 ∈ 𝑦 ) → 𝑦 ⊆ 𝐴 )
20		simpr	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝑦 )
21	19 20	sseldd	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝐴 )
22	21	adantll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝐴 )
23		simpll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝜑 )
24	23 22 3	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
25	4	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
26	22 24 25	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
27	26	ex	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑥 ∈ 𝑦 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 ) )
28	17 27	ralrimi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∀ 𝑥 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
29		sumeq2	⊢ ( ∀ 𝑥 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 → Σ 𝑥 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = Σ 𝑥 ∈ 𝑦 𝐵 )
30	28 29	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑥 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = Σ 𝑥 ∈ 𝑦 𝐵 )
31	15 30	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) = Σ 𝑥 ∈ 𝑦 𝐵 )
32	31	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) = ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑥 ∈ 𝑦 𝐵 ) )
33	32	rneqd	⊢ ( 𝜑 → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) = ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑥 ∈ 𝑦 𝐵 ) )
34	33	supeq1d	⊢ ( 𝜑 → sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) , ℝ^* , < ) = sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑥 ∈ 𝑦 𝐵 ) , ℝ^* , < ) )
35	6 34	eqtrd	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑥 ∈ 𝑦 𝐵 ) , ℝ^* , < ) )

Metamath Proof Explorer

Theorem sge0revalmpt

Proof