Metamath Proof Explorer


Theorem isrnmeas

Description: The property of being a measure on an undefined base sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion isrnmeas M ran measures dom M ran sigAlgebra M : dom M 0 +∞ M = 0 x 𝒫 dom M x ω Disj y x y M x = * y x M y

Proof

Step Hyp Ref Expression
1 df-meas measures = s ran sigAlgebra m | m : s 0 +∞ m = 0 x 𝒫 s x ω Disj y x y m x = * y x m y
2 vex s V
3 ovex 0 +∞ V
4 mapex s V 0 +∞ V m | m : s 0 +∞ V
5 2 3 4 mp2an m | m : s 0 +∞ V
6 simp1 m : s 0 +∞ m = 0 x 𝒫 s x ω Disj y x y m x = * y x m y m : s 0 +∞
7 6 ss2abi m | m : s 0 +∞ m = 0 x 𝒫 s x ω Disj y x y m x = * y x m y m | m : s 0 +∞
8 5 7 ssexi m | m : s 0 +∞ m = 0 x 𝒫 s x ω Disj y x y m x = * y x m y V
9 feq1 m = M m : s 0 +∞ M : s 0 +∞
10 fveq1 m = M m = M
11 10 eqeq1d m = M m = 0 M = 0
12 fveq1 m = M m x = M x
13 fveq1 m = M m y = M y
14 13 esumeq2sdv m = M * y x m y = * y x M y
15 12 14 eqeq12d m = M m x = * y x m y M x = * y x M y
16 15 imbi2d m = M x ω Disj y x y m x = * y x m y x ω Disj y x y M x = * y x M y
17 16 ralbidv m = M x 𝒫 s x ω Disj y x y m x = * y x m y x 𝒫 s x ω Disj y x y M x = * y x M y
18 9 11 17 3anbi123d m = M m : s 0 +∞ m = 0 x 𝒫 s x ω Disj y x y m x = * y x m y M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y
19 1 8 18 abfmpunirn M ran measures M V s ran sigAlgebra M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y
20 19 simprbi M ran measures s ran sigAlgebra M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y
21 fdm M : s 0 +∞ dom M = s
22 21 3ad2ant1 M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y dom M = s
23 22 adantl s ran sigAlgebra M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y dom M = s
24 simpl s ran sigAlgebra M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y s ran sigAlgebra
25 23 24 eqeltrd s ran sigAlgebra M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y dom M ran sigAlgebra
26 simp1 M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y M : s 0 +∞
27 feq2 dom M = s M : dom M 0 +∞ M : s 0 +∞
28 27 biimpar dom M = s M : s 0 +∞ M : dom M 0 +∞
29 22 26 28 syl2anc M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y M : dom M 0 +∞
30 simp2 M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y M = 0
31 simp3 M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y x 𝒫 s x ω Disj y x y M x = * y x M y
32 pweq dom M = s 𝒫 dom M = 𝒫 s
33 32 raleqdv dom M = s x 𝒫 dom M x ω Disj y x y M x = * y x M y x 𝒫 s x ω Disj y x y M x = * y x M y
34 33 biimpar dom M = s x 𝒫 s x ω Disj y x y M x = * y x M y x 𝒫 dom M x ω Disj y x y M x = * y x M y
35 22 31 34 syl2anc M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y x 𝒫 dom M x ω Disj y x y M x = * y x M y
36 29 30 35 3jca M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y M : dom M 0 +∞ M = 0 x 𝒫 dom M x ω Disj y x y M x = * y x M y
37 36 adantl s ran sigAlgebra M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y M : dom M 0 +∞ M = 0 x 𝒫 dom M x ω Disj y x y M x = * y x M y
38 25 37 jca s ran sigAlgebra M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y dom M ran sigAlgebra M : dom M 0 +∞ M = 0 x 𝒫 dom M x ω Disj y x y M x = * y x M y
39 38 rexlimiva s ran sigAlgebra M : s 0 +∞ M = 0 x 𝒫 s x ω Disj y x y M x = * y x M y dom M ran sigAlgebra M : dom M 0 +∞ M = 0 x 𝒫 dom M x ω Disj y x y M x = * y x M y
40 20 39 syl M ran measures dom M ran sigAlgebra M : dom M 0 +∞ M = 0 x 𝒫 dom M x ω Disj y x y M x = * y x M y