Theorem esumcl 30924

Description: Closure for extended sum in the extended positive reals. (Contributed by Thierry Arnoux, 2-Jan-2017.)

Hypothesis

Ref	Expression
esumcl.1	⊢ Ⅎ𝑘𝐴

Assertion

Ref	Expression
esumcl	⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 ∈ (0[,]+∞))

Distinct variable group:   𝑘,𝑉

Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑘)

Proof of Theorem esumcl

Step	Hyp	Ref	Expression
1		xrge0base 30395	. . 3 ⊢ (0[,]+∞) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞)))
2		xrge0cmn 20283	. . . 4 ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd
3	2	a1i 11	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd)
4		xrge0tps 30820	. . . 4 ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp
5	4	a1i 11	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp)
6		simpl 475	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → 𝐴 ∈ 𝑉)
7		esumcl.1	. . . . . 6 ⊢ Ⅎ𝑘𝐴
8	7	nfel1 2943	. . . . 5 ⊢ Ⅎ𝑘 𝐴 ∈ 𝑉
9		nfra1 3166	. . . . 5 ⊢ Ⅎ𝑘∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)
10	8, 9	nfan 1862	. . . 4 ⊢ Ⅎ𝑘(𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞))
11		nfcv 2929	. . . 4 ⊢ Ⅎ𝑘(0[,]+∞)
12		simpr 477	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞))
13	12	r19.21bi 3155	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
14		eqid 2775	. . . 4 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)
15	10, 7, 11, 13, 14	fmptdF 30157	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞))
16	1, 3, 5, 6, 15	tsmscl 22440	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) ⊆ (0[,]+∞))
17		df-esum 30922	. . 3 ⊢ Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵))
18		eqid 2775	. . . 4 ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) = (ℝ*𝑠 ↾s (0[,]+∞))
19	18, 6, 15	xrge0tsmsbi 30522	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → (Σ*𝑘 ∈ 𝐴𝐵 ∈ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) ↔ Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵))))
20	17, 19	mpbiri 250	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 ∈ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)))
21	16, 20	sseldd 3858	1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 ∈ (0[,]+∞))

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507   ∈ wcel 2048  Ⅎwnfc 2913  ∀wral 3085  ∪ cuni 4710   ↦ cmpt 5006  (class class class)co 6974  0cc0 10331  +∞cpnf 10467  [,]cicc 12554   ↾_s cress 16334  ℝ^*_𝑠cxrs 16623  CMndccmn 18660  TopSpctps 21238   tsums ctsu 22431  Σ^*cesum 30921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-rep 5047  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277  ax-cnex 10387  ax-resscn 10388  ax-1cn 10389  ax-icn 10390  ax-addcl 10391  ax-addrcl 10392  ax-mulcl 10393  ax-mulrcl 10394  ax-mulcom 10395  ax-addass 10396  ax-mulass 10397  ax-distr 10398  ax-i2m1 10399  ax-1ne0 10400  ax-1rid 10401  ax-rnegex 10402  ax-rrecex 10403  ax-cnre 10404  ax-pre-lttri 10405  ax-pre-lttrn 10406  ax-pre-ltadd 10407  ax-pre-mulgt0 10408  ax-pre-sup 10409

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-nel 3071  df-ral 3090  df-rex 3091  df-reu 3092  df-rmo 3093  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-pss 3844  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-tp 4444  df-op 4446  df-uni 4711  df-int 4748  df-iun 4792  df-iin 4793  df-br 4928  df-opab 4990  df-mpt 5007  df-tr 5029  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-se 5364  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-isom 6195  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-of 7225  df-om 7395  df-1st 7498  df-2nd 7499  df-supp 7631  df-wrecs 7747  df-recs 7809  df-rdg 7847  df-1o 7901  df-oadd 7905  df-er 8085  df-map 8204  df-en 8303  df-dom 8304  df-sdom 8305  df-fin 8306  df-fsupp 8625  df-fi 8666  df-sup 8697  df-inf 8698  df-oi 8765  df-card 9158  df-pnf 10472  df-mnf 10473  df-xr 10474  df-ltxr 10475  df-le 10476  df-sub 10668  df-neg 10669  df-div 11095  df-nn 11436  df-2 11500  df-3 11501  df-4 11502  df-5 11503  df-6 11504  df-7 11505  df-8 11506  df-9 11507  df-n0 11705  df-z 11791  df-dec 11909  df-uz 12056  df-q 12160  df-xadd 12322  df-ioo 12555  df-ioc 12556  df-ico 12557  df-icc 12558  df-fz 12706  df-fzo 12847  df-seq 13182  df-hash 13503  df-struct 16335  df-ndx 16336  df-slot 16337  df-base 16339  df-sets 16340  df-ress 16341  df-plusg 16428  df-mulr 16429  df-tset 16434  df-ple 16435  df-ds 16437  df-rest 16546  df-topn 16547  df-0g 16565  df-gsum 16566  df-topgen 16567  df-ordt 16624  df-xrs 16625  df-mre 16709  df-mrc 16710  df-acs 16712  df-ps 17662  df-tsr 17663  df-mgm 17704  df-sgrp 17746  df-mnd 17757  df-submnd 17798  df-cntz 18212  df-cmn 18662  df-fbas 20238  df-fg 20239  df-top 21200  df-topon 21217  df-topsp 21239  df-bases 21252  df-ntr 21326  df-nei 21404  df-cn 21533  df-haus 21621  df-fil 22152  df-fm 22244  df-flim 22245  df-flf 22246  df-tsms 22432  df-esum 30922

This theorem is referenced by:  esumel  30941  esummono  30948  esumpad  30949  esumpad2  30950  esumle  30952  esumlef  30956  esumrnmpt2  30962  esumfsup  30964  esumpinfval  30967  esumpinfsum  30971  esumpmono  30973  esummulc1  30975  esummulc2  30976  esumdivc  30977  hasheuni  30979  esumcvg  30980  esumgect  30984  esum2dlem  30986  esum2d  30987  measiun  31113  omscl  31189  oms0  31191  omsmon  31192  omssubadd  31194  carsggect  31212  carsgclctunlem2  31213  omsmeas  31217