Theorem sge0val 44727

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

Assertion

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

Distinct variable groups:   𝑤,𝐹,𝑦   𝑦,𝑋

Allowed substitution hints:   𝑉(𝑦,𝑤)   𝑋(𝑤)

Proof of Theorem sge0val

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-sumge0 44724	. . 3 ⊢ Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < )))
2	1	a1i 11	. 2 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < ))))
3		rneq 5896	. . . . 5 ⊢ (𝑥 = 𝐹 → ran 𝑥 = ran 𝐹)
4	3	eleq2d 2818	. . . 4 ⊢ (𝑥 = 𝐹 → (+∞ ∈ ran 𝑥 ↔ +∞ ∈ ran 𝐹))
5	4	adantl 482	. . 3 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → (+∞ ∈ ran 𝑥 ↔ +∞ ∈ ran 𝐹))
6		dmeq 5864	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐹 → dom 𝑥 = dom 𝐹)
7	6	adantl 482	. . . . . . . . . . 11 ⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 = 𝐹) → dom 𝑥 = dom 𝐹)
8		fdm 6682	. . . . . . . . . . . 12 ⊢ (𝐹:𝑋⟶(0[,]+∞) → dom 𝐹 = 𝑋)
9	8	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 = 𝐹) → dom 𝐹 = 𝑋)
10	7, 9	eqtrd 2771	. . . . . . . . . 10 ⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 = 𝐹) → dom 𝑥 = 𝑋)
11	10	pweqd 4582	. . . . . . . . 9 ⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 = 𝐹) → 𝒫 dom 𝑥 = 𝒫 𝑋)
12	11	ineq1d 4176	. . . . . . . 8 ⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 = 𝐹) → (𝒫 dom 𝑥 ∩ Fin) = (𝒫 𝑋 ∩ Fin))
13	12	mpteq1d 5205	. . . . . . 7 ⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 = 𝐹) → (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) = (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)))
14	13	adantll 712	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) = (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)))
15		fveq1 6846	. . . . . . . . 9 ⊢ (𝑥 = 𝐹 → (𝑥‘𝑤) = (𝐹‘𝑤))
16	15	sumeq2sdv 15600	. . . . . . . 8 ⊢ (𝑥 = 𝐹 → Σ𝑤 ∈ 𝑦 (𝑥‘𝑤) = Σ𝑤 ∈ 𝑦 (𝐹‘𝑤))
17	16	mpteq2dv 5212	. . . . . . 7 ⊢ (𝑥 = 𝐹 → (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) = (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)))
18	17	adantl 482	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) = (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)))
19	14, 18	eqtrd 2771	. . . . 5 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) = (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)))
20	19	rneqd 5898	. . . 4 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) = ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)))
21	20	supeq1d 9391	. . 3 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < ) = sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < ))
22	5, 21	ifbieq2d 4517	. 2 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) ∧ 𝑥 = 𝐹) → if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < )) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < )))
23		simpr 485	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → 𝐹:𝑋⟶(0[,]+∞))
24		simpl 483	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → 𝑋 ∈ 𝑉)
25	23, 24	fexd 7182	. 2 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → 𝐹 ∈ V)
26		pnfxr 11218	. . . 4 ⊢ +∞ ∈ ℝ*
27	26	a1i 11	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → +∞ ∈ ℝ*)
28		xrltso 13070	. . . . 5 ⊢ < Or ℝ*
29	28	supex 9408	. . . 4 ⊢ sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < ) ∈ V
30	29	a1i 11	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < ) ∈ V)
31	27, 30	ifexd 4539	. 2 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < )) ∈ V)
32	2, 22, 25, 31	fvmptd 6960	1 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < )))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3446   ∩ cin 3912  ifcif 4491  𝒫 cpw 4565   ↦ cmpt 5193  dom cdm 5638  ran crn 5639  ⟶wf 6497  ‘cfv 6501  (class class class)co 7362  Fincfn 8890  supcsup 9385  0cc0 11060  +∞cpnf 11195  ℝ^*cxr 11197   < clt 11198  [,]cicc 13277  Σcsu 15582  Σ^{^}csumge0 44723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11116  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1ne0 11129  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136  ax-pre-mulgt0 11137

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-sup 9387  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204  df-sub 11396  df-neg 11397  df-nn 12163  df-n0 12423  df-z 12509  df-uz 12773  df-fz 13435  df-seq 13917  df-sum 15583  df-sumge0 44724

This theorem is referenced by:  sge0vald  44730