Metamath Proof Explorer

Theorem ismbl

Description: The predicate " A is Lebesgue-measurable". A set is measurable if it splits every other set x in a "nice" way, that is, if the measure of the pieces x i^i A and x \ A sum up to the measure of x (assuming that the measure of x is a real number, so that this addition makes sense). (Contributed by Mario Carneiro, 17-Mar-2014)

Ref Expression
Assertion ismbl 
|- ( A e. dom vol <-> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ineq2 
 |-  ( y = A -> ( x i^i y ) = ( x i^i A ) )
2 1 fveq2d 
 |-  ( y = A -> ( vol* ` ( x i^i y ) ) = ( vol* ` ( x i^i A ) ) )
3 difeq2 
 |-  ( y = A -> ( x \ y ) = ( x \ A ) )
4 3 fveq2d 
 |-  ( y = A -> ( vol* ` ( x \ y ) ) = ( vol* ` ( x \ A ) ) )
5 2 4 oveq12d 
 |-  ( y = A -> ( ( vol* ` ( x i^i y ) ) + ( vol* ` ( x \ y ) ) ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) )
6 5 eqeq2d 
 |-  ( y = A -> ( ( vol* ` x ) = ( ( vol* ` ( x i^i y ) ) + ( vol* ` ( x \ y ) ) ) <-> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) )
7 6 ralbidv 
 |-  ( y = A -> ( A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i y ) ) + ( vol* ` ( x \ y ) ) ) <-> A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) )
8 df-vol 
 |-  vol = ( vol* |` { y | A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i y ) ) + ( vol* ` ( x \ y ) ) ) } )
9 8 dmeqi 
 |-  dom vol = dom ( vol* |` { y | A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i y ) ) + ( vol* ` ( x \ y ) ) ) } )
10 dmres 
 |-  dom ( vol* |` { y | A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i y ) ) + ( vol* ` ( x \ y ) ) ) } ) = ( { y | A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i y ) ) + ( vol* ` ( x \ y ) ) ) } i^i dom vol* )
11 ovolf 
 |-  vol* : ~P RR --> ( 0 [,] +oo )
12 11 fdmi 
 |-  dom vol* = ~P RR
13 12 ineq2i 
 |-  ( { y | A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i y ) ) + ( vol* ` ( x \ y ) ) ) } i^i dom vol* ) = ( { y | A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i y ) ) + ( vol* ` ( x \ y ) ) ) } i^i ~P RR )
14 9 10 13 3eqtri 
 |-  dom vol = ( { y | A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i y ) ) + ( vol* ` ( x \ y ) ) ) } i^i ~P RR )
15 dfrab2 
 |-  { y e. ~P RR | A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i y ) ) + ( vol* ` ( x \ y ) ) ) } = ( { y | A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i y ) ) + ( vol* ` ( x \ y ) ) ) } i^i ~P RR )
16 14 15 eqtr4i 
 |-  dom vol = { y e. ~P RR | A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i y ) ) + ( vol* ` ( x \ y ) ) ) }
17 7 16 elrab2 
 |-  ( A e. dom vol <-> ( A e. ~P RR /\ A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) )
18 reex 
 |-  RR e. _V
19 18 elpw2 
 |-  ( A e. ~P RR <-> A C_ RR )
20 ffn 
 |-  ( vol* : ~P RR --> ( 0 [,] +oo ) -> vol* Fn ~P RR )
21 elpreima 
 |-  ( vol* Fn ~P RR -> ( x e. ( `' vol* " RR ) <-> ( x e. ~P RR /\ ( vol* ` x ) e. RR ) ) )
22 11 20 21 mp2b 
 |-  ( x e. ( `' vol* " RR ) <-> ( x e. ~P RR /\ ( vol* ` x ) e. RR ) )
23 22 imbi1i 
 |-  ( ( x e. ( `' vol* " RR ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) <-> ( ( x e. ~P RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) )
24 impexp 
 |-  ( ( ( x e. ~P RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) <-> ( x e. ~P RR -> ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) ) )
25 23 24 bitri 
 |-  ( ( x e. ( `' vol* " RR ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) <-> ( x e. ~P RR -> ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) ) )
26 25 ralbii2 
 |-  ( A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <-> A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) )
27 19 26 anbi12i 
 |-  ( ( A e. ~P RR /\ A. x e. ( `' vol* " RR ) ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) <-> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) ) )
28 17 27 bitri 
 |-  ( A e. dom vol <-> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) ) )