Metamath Proof Explorer

Theorem volmeas

Description: The Lebesgue measure is a measure. (Contributed by Thierry Arnoux, 16-Oct-2017)

Ref Expression
Assertion volmeas 
|- vol e. ( measures ` dom vol )

Proof

Step Hyp Ref Expression
1 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
2 fvssunirn 
 |-  ( sigAlgebra ` RR ) C_ U. ran sigAlgebra
3 dmvlsiga 
 |-  dom vol e. ( sigAlgebra ` RR )
4 2 3 sselii 
 |-  dom vol e. U. ran sigAlgebra
5 0elsiga 
 |-  ( dom vol e. U. ran sigAlgebra -> (/) e. dom vol )
6 4 5 ax-mp 
 |-  (/) e. dom vol
7 mblvol 
 |-  ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
8 6 7 ax-mp 
 |-  ( vol ` (/) ) = ( vol* ` (/) )
9 ovol0 
 |-  ( vol* ` (/) ) = 0
10 8 9 eqtri 
 |-  ( vol ` (/) ) = 0
11 simpr 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) -> x e. Fin )
12 nfv 
 |-  F/ y x e. ~P dom vol
13 nfv 
 |-  F/ y x ~<_ _om
14 nfdisj1 
 |-  F/ y Disj_ y e. x y
15 13 14 nfan 
 |-  F/ y ( x ~<_ _om /\ Disj_ y e. x y )
16 12 15 nfan 
 |-  F/ y ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) )
17 nfv 
 |-  F/ y x e. Fin
18 16 17 nfan 
 |-  F/ y ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin )
19 elpwi 
 |-  ( x e. ~P dom vol -> x C_ dom vol )
20 19 ad3antrrr 
 |-  ( ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) /\ y e. x ) -> x C_ dom vol )
21 simpr 
 |-  ( ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) /\ y e. x ) -> y e. x )
22 20 21 sseldd 
 |-  ( ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) /\ y e. x ) -> y e. dom vol )
23 22 ex 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) -> ( y e. x -> y e. dom vol ) )
24 18 23 ralrimi 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) -> A. y e. x y e. dom vol )
25 simplrr 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) -> Disj_ y e. x y )
26 uniiun 
 |-  U. x = U_ y e. x y
27 26 fveq2i 
 |-  ( vol ` U. x ) = ( vol ` U_ y e. x y )
28 volfiniune 
 |-  ( ( x e. Fin /\ A. y e. x y e. dom vol /\ Disj_ y e. x y ) -> ( vol ` U_ y e. x y ) = sum* y e. x ( vol ` y ) )
29 27 28 eqtrid 
 |-  ( ( x e. Fin /\ A. y e. x y e. dom vol /\ Disj_ y e. x y ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) )
30 11 24 25 29 syl3anc 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x e. Fin ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) )
31 bren 
 |-  ( NN ~~ x <-> E. f f : NN -1-1-onto-> x )
32 nfv 
 |-  F/ n ( x e. ~P dom vol /\ f : NN -1-1-onto-> x )
33 nfcv 
 |-  F/_ n ( vol ` y )
34 nfcv 
 |-  F/_ y ( vol ` ( f ` n ) )
35 nfcv 
 |-  F/_ n x
36 nfcv 
 |-  F/_ n NN
37 nfcv 
 |-  F/_ n f
38 fveq2 
 |-  ( y = ( f ` n ) -> ( vol ` y ) = ( vol ` ( f ` n ) ) )
39 simpl 
 |-  ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) -> x e. ~P dom vol )
40 simpr 
 |-  ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) -> f : NN -1-1-onto-> x )
41 eqidd 
 |-  ( ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) /\ n e. NN ) -> ( f ` n ) = ( f ` n ) )
42 1 a1i 
 |-  ( ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) /\ y e. x ) -> vol : dom vol --> ( 0 [,] +oo ) )
43 39 19 syl 
 |-  ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) -> x C_ dom vol )
44 43 sselda 
 |-  ( ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) /\ y e. x ) -> y e. dom vol )
45 42 44 ffvelcdmd 
 |-  ( ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) /\ y e. x ) -> ( vol ` y ) e. ( 0 [,] +oo ) )
46 32 33 34 35 36 37 38 39 40 41 45 esumf1o 
 |-  ( ( x e. ~P dom vol /\ f : NN -1-1-onto-> x ) -> sum* y e. x ( vol ` y ) = sum* n e. NN ( vol ` ( f ` n ) ) )
47 46 adantlr 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> sum* y e. x ( vol ` y ) = sum* n e. NN ( vol ` ( f ` n ) ) )
48 19 ad3antrrr 
 |-  ( ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) /\ n e. NN ) -> x C_ dom vol )
49 f1of 
 |-  ( f : NN -1-1-onto-> x -> f : NN --> x )
50 49 adantl 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> f : NN --> x )
51 50 ffvelcdmda 
 |-  ( ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) /\ n e. NN ) -> ( f ` n ) e. x )
52 48 51 sseldd 
 |-  ( ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) /\ n e. NN ) -> ( f ` n ) e. dom vol )
53 52 ralrimiva 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> A. n e. NN ( f ` n ) e. dom vol )
54 simpr 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> f : NN -1-1-onto-> x )
55 simplrr 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> Disj_ y e. x y )
56 id 
 |-  ( f : NN -1-1-onto-> x -> f : NN -1-1-onto-> x )
57 simpr 
 |-  ( ( f : NN -1-1-onto-> x /\ y = ( f ` n ) ) -> y = ( f ` n ) )
58 56 57 disjrdx 
 |-  ( f : NN -1-1-onto-> x -> ( Disj_ n e. NN ( f ` n ) <-> Disj_ y e. x y ) )
59 58 biimpar 
 |-  ( ( f : NN -1-1-onto-> x /\ Disj_ y e. x y ) -> Disj_ n e. NN ( f ` n ) )
60 54 55 59 syl2anc 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> Disj_ n e. NN ( f ` n ) )
61 voliune 
 |-  ( ( A. n e. NN ( f ` n ) e. dom vol /\ Disj_ n e. NN ( f ` n ) ) -> ( vol ` U_ n e. NN ( f ` n ) ) = sum* n e. NN ( vol ` ( f ` n ) ) )
62 53 60 61 syl2anc 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> ( vol ` U_ n e. NN ( f ` n ) ) = sum* n e. NN ( vol ` ( f ` n ) ) )
63 f1ofo 
 |-  ( f : NN -1-1-onto-> x -> f : NN -onto-> x )
64 63 57 iunrdx 
 |-  ( f : NN -1-1-onto-> x -> U_ n e. NN ( f ` n ) = U_ y e. x y )
65 64 26 eqtr4di 
 |-  ( f : NN -1-1-onto-> x -> U_ n e. NN ( f ` n ) = U. x )
66 65 fveq2d 
 |-  ( f : NN -1-1-onto-> x -> ( vol ` U_ n e. NN ( f ` n ) ) = ( vol ` U. x ) )
67 66 adantl 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> ( vol ` U_ n e. NN ( f ` n ) ) = ( vol ` U. x ) )
68 47 62 67 3eqtr2rd 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ f : NN -1-1-onto-> x ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) )
69 68 ex 
 |-  ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( f : NN -1-1-onto-> x -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) )
70 69 exlimdv 
 |-  ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( E. f f : NN -1-1-onto-> x -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) )
71 70 imp 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ E. f f : NN -1-1-onto-> x ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) )
72 31 71 sylan2b 
 |-  ( ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ NN ~~ x ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) )
73 brdom2 
 |-  ( x ~<_ _om <-> ( x ~< _om \/ x ~~ _om ) )
74 73 biimpi 
 |-  ( x ~<_ _om -> ( x ~< _om \/ x ~~ _om ) )
75 isfinite2 
 |-  ( x ~< _om -> x e. Fin )
76 ensymb 
 |-  ( x ~~ _om <-> _om ~~ x )
77 nnenom 
 |-  NN ~~ _om
78 entr 
 |-  ( ( NN ~~ _om /\ _om ~~ x ) -> NN ~~ x )
79 77 78 mpan 
 |-  ( _om ~~ x -> NN ~~ x )
80 76 79 sylbi 
 |-  ( x ~~ _om -> NN ~~ x )
81 75 80 orim12i 
 |-  ( ( x ~< _om \/ x ~~ _om ) -> ( x e. Fin \/ NN ~~ x ) )
82 74 81 syl 
 |-  ( x ~<_ _om -> ( x e. Fin \/ NN ~~ x ) )
83 82 ad2antrl 
 |-  ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( x e. Fin \/ NN ~~ x ) )
84 30 72 83 mpjaodan 
 |-  ( ( x e. ~P dom vol /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) )
85 84 ex 
 |-  ( x e. ~P dom vol -> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) )
86 85 rgen 
 |-  A. x e. ~P dom vol ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) )
87 ismeas 
 |-  ( dom vol e. U. ran sigAlgebra -> ( vol e. ( measures ` dom vol ) <-> ( vol : dom vol --> ( 0 [,] +oo ) /\ ( vol ` (/) ) = 0 /\ A. x e. ~P dom vol ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) ) ) )
88 4 87 ax-mp 
 |-  ( vol e. ( measures ` dom vol ) <-> ( vol : dom vol --> ( 0 [,] +oo ) /\ ( vol ` (/) ) = 0 /\ A. x e. ~P dom vol ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( vol ` U. x ) = sum* y e. x ( vol ` y ) ) ) )
89 1 10 86 88 mpbir3an 
 |-  vol e. ( measures ` dom vol )