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

Theorem ismeas 33197
Description: The property of being a measure. (Contributed by Thierry Arnoux, 10-Sep-2016.) (Revised by Thierry Arnoux, 19-Oct-2016.)
Assertion
Ref Expression
ismeas (𝑆 ∈ βˆͺ ran sigAlgebra β†’ (𝑀 ∈ (measuresβ€˜π‘†) ↔ (𝑀:π‘†βŸΆ(0[,]+∞) ∧ (π‘€β€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑆((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘€β€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦)))))
Distinct variable groups:   π‘₯,𝑦,𝑀   π‘₯,𝑆
Allowed substitution hint:   𝑆(𝑦)

Proof of Theorem ismeas
Dummy variables π‘š 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3493 . . 3 (𝑀 ∈ (measuresβ€˜π‘†) β†’ 𝑀 ∈ V)
21a1i 11 . 2 (𝑆 ∈ βˆͺ ran sigAlgebra β†’ (𝑀 ∈ (measuresβ€˜π‘†) β†’ 𝑀 ∈ V))
3 simp1 1137 . . 3 ((𝑀:π‘†βŸΆ(0[,]+∞) ∧ (π‘€β€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑆((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘€β€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦))) β†’ 𝑀:π‘†βŸΆ(0[,]+∞))
4 ovex 7442 . . . 4 (0[,]+∞) ∈ V
5 fex2 7924 . . . . . 6 ((𝑀:π‘†βŸΆ(0[,]+∞) ∧ 𝑆 ∈ βˆͺ ran sigAlgebra ∧ (0[,]+∞) ∈ V) β†’ 𝑀 ∈ V)
653expb 1121 . . . . 5 ((𝑀:π‘†βŸΆ(0[,]+∞) ∧ (𝑆 ∈ βˆͺ ran sigAlgebra ∧ (0[,]+∞) ∈ V)) β†’ 𝑀 ∈ V)
76expcom 415 . . . 4 ((𝑆 ∈ βˆͺ ran sigAlgebra ∧ (0[,]+∞) ∈ V) β†’ (𝑀:π‘†βŸΆ(0[,]+∞) β†’ 𝑀 ∈ V))
84, 7mpan2 690 . . 3 (𝑆 ∈ βˆͺ ran sigAlgebra β†’ (𝑀:π‘†βŸΆ(0[,]+∞) β†’ 𝑀 ∈ V))
93, 8syl5 34 . 2 (𝑆 ∈ βˆͺ ran sigAlgebra β†’ ((𝑀:π‘†βŸΆ(0[,]+∞) ∧ (π‘€β€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑆((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘€β€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦))) β†’ 𝑀 ∈ V))
10 df-meas 33194 . . . 4 measures = (𝑠 ∈ βˆͺ ran sigAlgebra ↦ {π‘š ∣ (π‘š:π‘ βŸΆ(0[,]+∞) ∧ (π‘šβ€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘šβ€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦)))})
11 vex 3479 . . . . . 6 𝑠 ∈ V
12 mapex 8826 . . . . . 6 ((𝑠 ∈ V ∧ (0[,]+∞) ∈ V) β†’ {π‘š ∣ π‘š:π‘ βŸΆ(0[,]+∞)} ∈ V)
1311, 4, 12mp2an 691 . . . . 5 {π‘š ∣ π‘š:π‘ βŸΆ(0[,]+∞)} ∈ V
14 simp1 1137 . . . . . 6 ((π‘š:π‘ βŸΆ(0[,]+∞) ∧ (π‘šβ€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘šβ€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦))) β†’ π‘š:π‘ βŸΆ(0[,]+∞))
1514ss2abi 4064 . . . . 5 {π‘š ∣ (π‘š:π‘ βŸΆ(0[,]+∞) ∧ (π‘šβ€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘šβ€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦)))} βŠ† {π‘š ∣ π‘š:π‘ βŸΆ(0[,]+∞)}
1613, 15ssexi 5323 . . . 4 {π‘š ∣ (π‘š:π‘ βŸΆ(0[,]+∞) ∧ (π‘šβ€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘šβ€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦)))} ∈ V
17 simpr 486 . . . . . 6 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ π‘š = 𝑀)
18 simpl 484 . . . . . 6 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ 𝑠 = 𝑆)
1917, 18feq12d 6706 . . . . 5 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (π‘š:π‘ βŸΆ(0[,]+∞) ↔ 𝑀:π‘†βŸΆ(0[,]+∞)))
20 fveq1 6891 . . . . . . 7 (π‘š = 𝑀 β†’ (π‘šβ€˜βˆ…) = (π‘€β€˜βˆ…))
2120eqeq1d 2735 . . . . . 6 (π‘š = 𝑀 β†’ ((π‘šβ€˜βˆ…) = 0 ↔ (π‘€β€˜βˆ…) = 0))
2221adantl 483 . . . . 5 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ ((π‘šβ€˜βˆ…) = 0 ↔ (π‘€β€˜βˆ…) = 0))
2318pweqd 4620 . . . . . 6 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ 𝒫 𝑠 = 𝒫 𝑆)
24 fveq1 6891 . . . . . . . . 9 (π‘š = 𝑀 β†’ (π‘šβ€˜βˆͺ π‘₯) = (π‘€β€˜βˆͺ π‘₯))
25 fveq1 6891 . . . . . . . . . 10 (π‘š = 𝑀 β†’ (π‘šβ€˜π‘¦) = (π‘€β€˜π‘¦))
2625esumeq2sdv 33037 . . . . . . . . 9 (π‘š = 𝑀 β†’ Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦) = Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦))
2724, 26eqeq12d 2749 . . . . . . . 8 (π‘š = 𝑀 β†’ ((π‘šβ€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦) ↔ (π‘€β€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦)))
2827imbi2d 341 . . . . . . 7 (π‘š = 𝑀 β†’ (((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘šβ€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦)) ↔ ((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘€β€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦))))
2928adantl 483 . . . . . 6 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘šβ€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦)) ↔ ((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘€β€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦))))
3023, 29raleqbidv 3343 . . . . 5 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ (βˆ€π‘₯ ∈ 𝒫 𝑠((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘šβ€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦)) ↔ βˆ€π‘₯ ∈ 𝒫 𝑆((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘€β€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦))))
3119, 22, 303anbi123d 1437 . . . 4 ((𝑠 = 𝑆 ∧ π‘š = 𝑀) β†’ ((π‘š:π‘ βŸΆ(0[,]+∞) ∧ (π‘šβ€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘šβ€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦))) ↔ (𝑀:π‘†βŸΆ(0[,]+∞) ∧ (π‘€β€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑆((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘€β€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦)))))
3210, 16, 31abfmpel 31880 . . 3 ((𝑆 ∈ βˆͺ ran sigAlgebra ∧ 𝑀 ∈ V) β†’ (𝑀 ∈ (measuresβ€˜π‘†) ↔ (𝑀:π‘†βŸΆ(0[,]+∞) ∧ (π‘€β€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑆((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘€β€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦)))))
3332ex 414 . 2 (𝑆 ∈ βˆͺ ran sigAlgebra β†’ (𝑀 ∈ V β†’ (𝑀 ∈ (measuresβ€˜π‘†) ↔ (𝑀:π‘†βŸΆ(0[,]+∞) ∧ (π‘€β€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑆((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘€β€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦))))))
342, 9, 33pm5.21ndd 381 1 (𝑆 ∈ βˆͺ ran sigAlgebra β†’ (𝑀 ∈ (measuresβ€˜π‘†) ↔ (𝑀:π‘†βŸΆ(0[,]+∞) ∧ (π‘€β€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑆((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘€β€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦)))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {cab 2710  βˆ€wral 3062  Vcvv 3475  βˆ…c0 4323  π’« cpw 4603  βˆͺ cuni 4909  Disj wdisj 5114   class class class wbr 5149  ran crn 5678  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409  Ο‰com 7855   β‰Ό cdom 8937  0cc0 11110  +∞cpnf 11245  [,]cicc 13327  Ξ£*cesum 33025  sigAlgebracsiga 33106  measurescmeas 33193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-esum 33026  df-meas 33194
This theorem is referenced by:  measbasedom  33200  measfrge0  33201  measvnul  33204  measvun  33207  measinb  33219  measres  33220  measdivcst  33222  measdivcstALTV  33223  cntmeas  33224  volmeas  33229  ddemeas  33234  omsmeas  33322  dstrvprob  33470
  Copyright terms: Public domain W3C validator