Metamath Proof Explorer

Theorem nulmbl

Description: A nullset is measurable. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Assertion nulmbl 
|- ( ( A C_ RR /\ ( vol* ` A ) = 0 ) -> A e. dom vol )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A C_ RR /\ ( vol* ` A ) = 0 ) -> A C_ RR )
2 elpwi 
 |-  ( x e. ~P RR -> x C_ RR )
3 inss2 
 |-  ( x i^i A ) C_ A
4 ovolssnul 
 |-  ( ( ( x i^i A ) C_ A /\ A C_ RR /\ ( vol* ` A ) = 0 ) -> ( vol* ` ( x i^i A ) ) = 0 )
5 3 4 mp3an1 
 |-  ( ( A C_ RR /\ ( vol* ` A ) = 0 ) -> ( vol* ` ( x i^i A ) ) = 0 )
6 5 adantr 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) = 0 ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x i^i A ) ) = 0 )
7 6 oveq1d 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) = 0 ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) = ( 0 + ( vol* ` ( x \ A ) ) ) )
8 difss 
 |-  ( x \ A ) C_ x
9 ovolsscl 
 |-  ( ( ( x \ A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR )
10 8 9 mp3an1 
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR )
11 10 adantl 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) = 0 ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ A ) ) e. RR )
12 11 recnd 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) = 0 ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ A ) ) e. CC )
13 12 addlidd 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) = 0 ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( 0 + ( vol* ` ( x \ A ) ) ) = ( vol* ` ( x \ A ) ) )
14 7 13 eqtrd 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) = 0 ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) = ( vol* ` ( x \ A ) ) )
15 simprl 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) = 0 ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> x C_ RR )
16 ovolss 
 |-  ( ( ( x \ A ) C_ x /\ x C_ RR ) -> ( vol* ` ( x \ A ) ) <_ ( vol* ` x ) )
17 8 15 16 sylancr 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) = 0 ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ A ) ) <_ ( vol* ` x ) )
18 14 17 eqbrtrd 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) = 0 ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) )
19 18 expr 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) = 0 ) /\ x C_ RR ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) )
20 2 19 sylan2 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) = 0 ) /\ x e. ~P RR ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) )
21 20 ralrimiva 
 |-  ( ( A C_ RR /\ ( vol* ` A ) = 0 ) -> A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) )
22 ismbl2 
 |-  ( A e. dom vol <-> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) )
23 1 21 22 sylanbrc 
 |-  ( ( A C_ RR /\ ( vol* ` A ) = 0 ) -> A e. dom vol )