Metamath Proof Explorer

Theorem cmmbl

Description: The complement of a measurable set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Assertion cmmbl 
|- ( A e. dom vol -> ( RR \ A ) e. dom vol )

Proof

Step Hyp Ref Expression
1 difssd 
 |-  ( A e. dom vol -> ( RR \ A ) C_ RR )
2 elpwi 
 |-  ( x e. ~P RR -> x C_ RR )
3 inss1 
 |-  ( x i^i A ) C_ x
4 ovolsscl 
 |-  ( ( ( x i^i A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR )
5 3 4 mp3an1 
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR )
6 5 3adant1 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR )
7 6 recnd 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. CC )
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 3adant1 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR )
12 11 recnd 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. CC )
13 7 12 addcomd 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) = ( ( vol* ` ( x \ A ) ) + ( vol* ` ( x i^i A ) ) ) )
14 mblsplit 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) )
15 indifcom 
 |-  ( RR i^i ( x \ A ) ) = ( x i^i ( RR \ A ) )
16 simp2 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> x C_ RR )
17 16 ssdifssd 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x \ A ) C_ RR )
18 sseqin2 
 |-  ( ( x \ A ) C_ RR <-> ( RR i^i ( x \ A ) ) = ( x \ A ) )
19 17 18 sylib 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( RR i^i ( x \ A ) ) = ( x \ A ) )
20 15 19 eqtr3id 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x i^i ( RR \ A ) ) = ( x \ A ) )
21 20 fveq2d 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( RR \ A ) ) ) = ( vol* ` ( x \ A ) ) )
22 difin 
 |-  ( x \ ( x i^i ( RR \ A ) ) ) = ( x \ ( RR \ A ) )
23 20 difeq2d 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x \ ( x i^i ( RR \ A ) ) ) = ( x \ ( x \ A ) ) )
24 22 23 eqtr3id 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x \ ( RR \ A ) ) = ( x \ ( x \ A ) ) )
25 dfin4 
 |-  ( x i^i A ) = ( x \ ( x \ A ) )
26 24 25 eqtr4di 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x \ ( RR \ A ) ) = ( x i^i A ) )
27 26 fveq2d 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ ( RR \ A ) ) ) = ( vol* ` ( x i^i A ) ) )
28 21 27 oveq12d 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i ( RR \ A ) ) ) + ( vol* ` ( x \ ( RR \ A ) ) ) ) = ( ( vol* ` ( x \ A ) ) + ( vol* ` ( x i^i A ) ) ) )
29 13 14 28 3eqtr4d 
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i ( RR \ A ) ) ) + ( vol* ` ( x \ ( RR \ A ) ) ) ) )
30 29 3expia 
 |-  ( ( A e. dom vol /\ x C_ RR ) -> ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i ( RR \ A ) ) ) + ( vol* ` ( x \ ( RR \ A ) ) ) ) ) )
31 2 30 sylan2 
 |-  ( ( A e. dom vol /\ x e. ~P RR ) -> ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i ( RR \ A ) ) ) + ( vol* ` ( x \ ( RR \ A ) ) ) ) ) )
32 31 ralrimiva 
 |-  ( A e. dom vol -> A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i ( RR \ A ) ) ) + ( vol* ` ( x \ ( RR \ A ) ) ) ) ) )
33 ismbl 
 |-  ( ( RR \ A ) e. dom vol <-> ( ( RR \ A ) C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i ( RR \ A ) ) ) + ( vol* ` ( x \ ( RR \ A ) ) ) ) ) ) )
34 1 32 33 sylanbrc 
 |-  ( A e. dom vol -> ( RR \ A ) e. dom vol )