Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pmeasadd Structured version   Visualization version   GIF version

Theorem pmeasadd 33986
Description: A premeasure on a ring of sets is additive on disjoint countable collections. This is called sigma-additivity. (Contributed by Thierry Arnoux, 19-Jul-2020.)
Hypotheses
Ref Expression
caraext.1 (𝜑𝑃:𝑅⟶(0[,]+∞))
caraext.2 (𝜑 → (𝑃‘∅) = 0)
caraext.3 ((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥𝑅Disj 𝑦𝑥 𝑦)) → (𝑃 𝑥) = Σ*𝑦𝑥(𝑃𝑦))
pmeassubadd.q 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥𝑠𝑦𝑠 ((𝑥𝑦) ∈ 𝑠 ∧ (𝑥𝑦) ∈ 𝑠))}
pmeassubadd.1 (𝜑𝑅𝑄)
pmeassubadd.2 (𝜑𝐴 ≼ ω)
pmeassubadd.3 ((𝜑𝑘𝐴) → 𝐵𝑅)
pmeasadd.4 (𝜑Disj 𝑘𝐴 𝐵)
Assertion
Ref Expression
pmeasadd (𝜑 → (𝑃 𝑘𝐴 𝐵) = Σ*𝑘𝐴(𝑃𝐵))
Distinct variable groups:   𝑥,𝑃,𝑦   𝑥,𝑅,𝑦   𝜑,𝑥,𝑦   𝐴,𝑘,𝑥,𝑦   𝑥,𝐵,𝑦   𝑃,𝑘   𝑅,𝑘   𝜑,𝑘
Allowed substitution hints:   𝜑(𝑠)   𝐴(𝑠)   𝐵(𝑘,𝑠)   𝑃(𝑠)   𝑄(𝑥,𝑦,𝑘,𝑠)   𝑅(𝑠)   𝑂(𝑥,𝑦,𝑘,𝑠)

Proof of Theorem pmeasadd
StepHypRef Expression
1 pmeassubadd.3 . . . . 5 ((𝜑𝑘𝐴) → 𝐵𝑅)
21ralrimiva 3143 . . . 4 (𝜑 → ∀𝑘𝐴 𝐵𝑅)
3 dfiun3g 5971 . . . 4 (∀𝑘𝐴 𝐵𝑅 𝑘𝐴 𝐵 = ran (𝑘𝐴𝐵))
42, 3syl 17 . . 3 (𝜑 𝑘𝐴 𝐵 = ran (𝑘𝐴𝐵))
54fveq2d 6906 . 2 (𝜑 → (𝑃 𝑘𝐴 𝐵) = (𝑃 ran (𝑘𝐴𝐵)))
6 pmeassubadd.2 . . . . . 6 (𝜑𝐴 ≼ ω)
7 mptct 10571 . . . . . 6 (𝐴 ≼ ω → (𝑘𝐴𝐵) ≼ ω)
8 rnct 10558 . . . . . 6 ((𝑘𝐴𝐵) ≼ ω → ran (𝑘𝐴𝐵) ≼ ω)
96, 7, 83syl 18 . . . . 5 (𝜑 → ran (𝑘𝐴𝐵) ≼ ω)
10 eqid 2728 . . . . . . 7 (𝑘𝐴𝐵) = (𝑘𝐴𝐵)
1110rnmptss 7138 . . . . . 6 (∀𝑘𝐴 𝐵𝑅 → ran (𝑘𝐴𝐵) ⊆ 𝑅)
122, 11syl 17 . . . . 5 (𝜑 → ran (𝑘𝐴𝐵) ⊆ 𝑅)
13 pmeasadd.4 . . . . . 6 (𝜑Disj 𝑘𝐴 𝐵)
14 disjrnmpt 32404 . . . . . 6 (Disj 𝑘𝐴 𝐵Disj 𝑦 ∈ ran (𝑘𝐴𝐵)𝑦)
1513, 14syl 17 . . . . 5 (𝜑Disj 𝑦 ∈ ran (𝑘𝐴𝐵)𝑦)
169, 12, 153jca 1125 . . . 4 (𝜑 → (ran (𝑘𝐴𝐵) ≼ ω ∧ ran (𝑘𝐴𝐵) ⊆ 𝑅Disj 𝑦 ∈ ran (𝑘𝐴𝐵)𝑦))
1716ancli 547 . . 3 (𝜑 → (𝜑 ∧ (ran (𝑘𝐴𝐵) ≼ ω ∧ ran (𝑘𝐴𝐵) ⊆ 𝑅Disj 𝑦 ∈ ran (𝑘𝐴𝐵)𝑦)))
18 ctex 8992 . . . . 5 (𝐴 ≼ ω → 𝐴 ∈ V)
19 mptexg 7239 . . . . 5 (𝐴 ∈ V → (𝑘𝐴𝐵) ∈ V)
206, 18, 193syl 18 . . . 4 (𝜑 → (𝑘𝐴𝐵) ∈ V)
21 rnexg 7918 . . . 4 ((𝑘𝐴𝐵) ∈ V → ran (𝑘𝐴𝐵) ∈ V)
22 breq1 5155 . . . . . . . 8 (𝑥 = ran (𝑘𝐴𝐵) → (𝑥 ≼ ω ↔ ran (𝑘𝐴𝐵) ≼ ω))
23 sseq1 4007 . . . . . . . 8 (𝑥 = ran (𝑘𝐴𝐵) → (𝑥𝑅 ↔ ran (𝑘𝐴𝐵) ⊆ 𝑅))
24 disjeq1 5124 . . . . . . . 8 (𝑥 = ran (𝑘𝐴𝐵) → (Disj 𝑦𝑥 𝑦Disj 𝑦 ∈ ran (𝑘𝐴𝐵)𝑦))
2522, 23, 243anbi123d 1432 . . . . . . 7 (𝑥 = ran (𝑘𝐴𝐵) → ((𝑥 ≼ ω ∧ 𝑥𝑅Disj 𝑦𝑥 𝑦) ↔ (ran (𝑘𝐴𝐵) ≼ ω ∧ ran (𝑘𝐴𝐵) ⊆ 𝑅Disj 𝑦 ∈ ran (𝑘𝐴𝐵)𝑦)))
2625anbi2d 628 . . . . . 6 (𝑥 = ran (𝑘𝐴𝐵) → ((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥𝑅Disj 𝑦𝑥 𝑦)) ↔ (𝜑 ∧ (ran (𝑘𝐴𝐵) ≼ ω ∧ ran (𝑘𝐴𝐵) ⊆ 𝑅Disj 𝑦 ∈ ran (𝑘𝐴𝐵)𝑦))))
27 unieq 4923 . . . . . . . 8 (𝑥 = ran (𝑘𝐴𝐵) → 𝑥 = ran (𝑘𝐴𝐵))
2827fveq2d 6906 . . . . . . 7 (𝑥 = ran (𝑘𝐴𝐵) → (𝑃 𝑥) = (𝑃 ran (𝑘𝐴𝐵)))
29 esumeq1 33694 . . . . . . 7 (𝑥 = ran (𝑘𝐴𝐵) → Σ*𝑦𝑥(𝑃𝑦) = Σ*𝑦 ∈ ran (𝑘𝐴𝐵)(𝑃𝑦))
3028, 29eqeq12d 2744 . . . . . 6 (𝑥 = ran (𝑘𝐴𝐵) → ((𝑃 𝑥) = Σ*𝑦𝑥(𝑃𝑦) ↔ (𝑃 ran (𝑘𝐴𝐵)) = Σ*𝑦 ∈ ran (𝑘𝐴𝐵)(𝑃𝑦)))
3126, 30imbi12d 343 . . . . 5 (𝑥 = ran (𝑘𝐴𝐵) → (((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥𝑅Disj 𝑦𝑥 𝑦)) → (𝑃 𝑥) = Σ*𝑦𝑥(𝑃𝑦)) ↔ ((𝜑 ∧ (ran (𝑘𝐴𝐵) ≼ ω ∧ ran (𝑘𝐴𝐵) ⊆ 𝑅Disj 𝑦 ∈ ran (𝑘𝐴𝐵)𝑦)) → (𝑃 ran (𝑘𝐴𝐵)) = Σ*𝑦 ∈ ran (𝑘𝐴𝐵)(𝑃𝑦))))
32 caraext.3 . . . . 5 ((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥𝑅Disj 𝑦𝑥 𝑦)) → (𝑃 𝑥) = Σ*𝑦𝑥(𝑃𝑦))
3331, 32vtoclg 3542 . . . 4 (ran (𝑘𝐴𝐵) ∈ V → ((𝜑 ∧ (ran (𝑘𝐴𝐵) ≼ ω ∧ ran (𝑘𝐴𝐵) ⊆ 𝑅Disj 𝑦 ∈ ran (𝑘𝐴𝐵)𝑦)) → (𝑃 ran (𝑘𝐴𝐵)) = Σ*𝑦 ∈ ran (𝑘𝐴𝐵)(𝑃𝑦)))
3420, 21, 333syl 18 . . 3 (𝜑 → ((𝜑 ∧ (ran (𝑘𝐴𝐵) ≼ ω ∧ ran (𝑘𝐴𝐵) ⊆ 𝑅Disj 𝑦 ∈ ran (𝑘𝐴𝐵)𝑦)) → (𝑃 ran (𝑘𝐴𝐵)) = Σ*𝑦 ∈ ran (𝑘𝐴𝐵)(𝑃𝑦)))
3517, 34mpd 15 . 2 (𝜑 → (𝑃 ran (𝑘𝐴𝐵)) = Σ*𝑦 ∈ ran (𝑘𝐴𝐵)(𝑃𝑦))
36 fveq2 6902 . . 3 (𝑦 = 𝐵 → (𝑃𝑦) = (𝑃𝐵))
376, 18syl 17 . . 3 (𝜑𝐴 ∈ V)
38 caraext.1 . . . . 5 (𝜑𝑃:𝑅⟶(0[,]+∞))
3938adantr 479 . . . 4 ((𝜑𝑘𝐴) → 𝑃:𝑅⟶(0[,]+∞))
4039, 1ffvelcdmd 7100 . . 3 ((𝜑𝑘𝐴) → (𝑃𝐵) ∈ (0[,]+∞))
41 fveq2 6902 . . . . 5 (𝐵 = ∅ → (𝑃𝐵) = (𝑃‘∅))
4241adantl 480 . . . 4 (((𝜑𝑘𝐴) ∧ 𝐵 = ∅) → (𝑃𝐵) = (𝑃‘∅))
43 caraext.2 . . . . 5 (𝜑 → (𝑃‘∅) = 0)
4443ad2antrr 724 . . . 4 (((𝜑𝑘𝐴) ∧ 𝐵 = ∅) → (𝑃‘∅) = 0)
4542, 44eqtrd 2768 . . 3 (((𝜑𝑘𝐴) ∧ 𝐵 = ∅) → (𝑃𝐵) = 0)
4636, 37, 40, 1, 45, 13esumrnmpt2 33728 . 2 (𝜑 → Σ*𝑦 ∈ ran (𝑘𝐴𝐵)(𝑃𝑦) = Σ*𝑘𝐴(𝑃𝐵))
475, 35, 463eqtrd 2772 1 (𝜑 → (𝑃 𝑘𝐴 𝐵) = Σ*𝑘𝐴(𝑃𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3058  {crab 3430  Vcvv 3473  cdif 3946  cun 3947  wss 3949  c0 4326  𝒫 cpw 4606   cuni 4912   ciun 5000  Disj wdisj 5117   class class class wbr 5152  cmpt 5235  ran crn 5683  wf 6549  cfv 6553  (class class class)co 7426  ωcom 7878  cdom 8970  0cc0 11148  +∞cpnf 11285  [,]cicc 13369  Σ*cesum 33687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-inf2 9674  ax-ac2 10496  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225  ax-pre-sup 11226  ax-addf 11227  ax-mulf 11228
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-disj 5118  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7692  df-om 7879  df-1st 8001  df-2nd 8002  df-supp 8174  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-2o 8496  df-er 8733  df-map 8855  df-pm 8856  df-ixp 8925  df-en 8973  df-dom 8974  df-sdom 8975  df-fin 8976  df-fsupp 9396  df-fi 9444  df-sup 9475  df-inf 9476  df-oi 9543  df-card 9972  df-acn 9975  df-ac 10149  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-div 11912  df-nn 12253  df-2 12315  df-3 12316  df-4 12317  df-5 12318  df-6 12319  df-7 12320  df-8 12321  df-9 12322  df-n0 12513  df-z 12599  df-dec 12718  df-uz 12863  df-q 12973  df-rp 13017  df-xneg 13134  df-xadd 13135  df-xmul 13136  df-ioo 13370  df-ioc 13371  df-ico 13372  df-icc 13373  df-fz 13527  df-fzo 13670  df-fl 13799  df-mod 13877  df-seq 14009  df-exp 14069  df-fac 14275  df-bc 14304  df-hash 14332  df-shft 15056  df-cj 15088  df-re 15089  df-im 15090  df-sqrt 15224  df-abs 15225  df-limsup 15457  df-clim 15474  df-rlim 15475  df-sum 15675  df-ef 16053  df-sin 16055  df-cos 16056  df-pi 16058  df-struct 17125  df-sets 17142  df-slot 17160  df-ndx 17172  df-base 17190  df-ress 17219  df-plusg 17255  df-mulr 17256  df-starv 17257  df-sca 17258  df-vsca 17259  df-ip 17260  df-tset 17261  df-ple 17262  df-ds 17264  df-unif 17265  df-hom 17266  df-cco 17267  df-rest 17413  df-topn 17414  df-0g 17432  df-gsum 17433  df-topgen 17434  df-pt 17435  df-prds 17438  df-ordt 17492  df-xrs 17493  df-qtop 17498  df-imas 17499  df-xps 17501  df-mre 17575  df-mrc 17576  df-acs 17578  df-ps 18567  df-tsr 18568  df-plusf 18608  df-mgm 18609  df-sgrp 18688  df-mnd 18704  df-mhm 18749  df-submnd 18750  df-grp 18907  df-minusg 18908  df-sbg 18909  df-mulg 19038  df-subg 19092  df-cntz 19282  df-cmn 19751  df-abl 19752  df-mgp 20089  df-rng 20107  df-ur 20136  df-ring 20189  df-cring 20190  df-subrng 20497  df-subrg 20522  df-abv 20711  df-lmod 20759  df-scaf 20760  df-sra 21072  df-rgmod 21073  df-psmet 21285  df-xmet 21286  df-met 21287  df-bl 21288  df-mopn 21289  df-fbas 21290  df-fg 21291  df-cnfld 21294  df-top 22824  df-topon 22841  df-topsp 22863  df-bases 22877  df-cld 22951  df-ntr 22952  df-cls 22953  df-nei 23030  df-lp 23068  df-perf 23069  df-cn 23159  df-cnp 23160  df-haus 23247  df-tx 23494  df-hmeo 23687  df-fil 23778  df-fm 23870  df-flim 23871  df-flf 23872  df-tmd 24004  df-tgp 24005  df-tsms 24059  df-trg 24092  df-xms 24254  df-ms 24255  df-tms 24256  df-nm 24519  df-ngp 24520  df-nrg 24522  df-nlm 24523  df-ii 24825  df-cncf 24826  df-limc 25823  df-dv 25824  df-log 26518  df-esum 33688
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator