Metamath Proof Explorer

Theorem volmea

Description: The Lebesgue measure on the Reals is actually a measure. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Assertion volmea 
|- ( ph -> vol e. Meas )

Proof

Step Hyp Ref Expression
1 dmvolsal 
 |-  dom vol e. SAlg
2 1 a1i 
 |-  ( ph -> dom vol e. SAlg )
3 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
4 3 a1i 
 |-  ( ph -> vol : dom vol --> ( 0 [,] +oo ) )
5 vol0 
 |-  ( vol ` (/) ) = 0
6 5 a1i 
 |-  ( ph -> ( vol ` (/) ) = 0 )
7 simp1 
 |-  ( ( ph /\ e : NN --> dom vol /\ Disj_ n e. NN ( e ` n ) ) -> ph )
8 simp2 
 |-  ( ( ph /\ e : NN --> dom vol /\ Disj_ n e. NN ( e ` n ) ) -> e : NN --> dom vol )
9 fveq2 
 |-  ( m = n -> ( e ` m ) = ( e ` n ) )
10 9 cbvdisjv 
 |-  ( Disj_ m e. NN ( e ` m ) <-> Disj_ n e. NN ( e ` n ) )
11 10 biimpri 
 |-  ( Disj_ n e. NN ( e ` n ) -> Disj_ m e. NN ( e ` m ) )
12 11 3ad2ant3 
 |-  ( ( ph /\ e : NN --> dom vol /\ Disj_ n e. NN ( e ` n ) ) -> Disj_ m e. NN ( e ` m ) )
13 simp2 
 |-  ( ( ph /\ e : NN --> dom vol /\ Disj_ m e. NN ( e ` m ) ) -> e : NN --> dom vol )
14 10 biimpi 
 |-  ( Disj_ m e. NN ( e ` m ) -> Disj_ n e. NN ( e ` n ) )
15 14 3ad2ant3 
 |-  ( ( ph /\ e : NN --> dom vol /\ Disj_ m e. NN ( e ` m ) ) -> Disj_ n e. NN ( e ` n ) )
16 13 15 voliunsge0 
 |-  ( ( ph /\ e : NN --> dom vol /\ Disj_ m e. NN ( e ` m ) ) -> ( vol ` U_ n e. NN ( e ` n ) ) = ( sum^ ` ( n e. NN |-> ( vol ` ( e ` n ) ) ) ) )
17 7 8 12 16 syl3anc 
 |-  ( ( ph /\ e : NN --> dom vol /\ Disj_ n e. NN ( e ` n ) ) -> ( vol ` U_ n e. NN ( e ` n ) ) = ( sum^ ` ( n e. NN |-> ( vol ` ( e ` n ) ) ) ) )
18 2 4 6 17 ismeannd 
 |-  ( ph -> vol e. Meas )