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 )