Metamath Proof Explorer

Theorem ismbl2

Description: From ovolun , it suffices to show that the measure of x is at least the sum of the measures of x i^i A and x \ A . (Contributed by Mario Carneiro, 15-Jun-2014)

Ref Expression
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 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 ) ) ) ) ) )
2 elpwi 
 |-  ( x e. ~P RR -> x C_ RR )
3 inundif 
 |-  ( ( x i^i A ) u. ( x \ A ) ) = x
4 3 fveq2i 
 |-  ( vol* ` ( ( x i^i A ) u. ( x \ A ) ) ) = ( vol* ` x )
5 inss1 
 |-  ( x i^i A ) C_ x
6 simprl 
 |-  ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> x C_ RR )
7 5 6 sstrid 
 |-  ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( x i^i A ) C_ RR )
8 ovolsscl 
 |-  ( ( ( x i^i A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR )
9 5 8 mp3an1 
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR )
10 9 adantl 
 |-  ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x i^i A ) ) e. RR )
11 difss 
 |-  ( x \ A ) C_ x
12 11 6 sstrid 
 |-  ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( x \ A ) C_ RR )
13 ovolsscl 
 |-  ( ( ( x \ A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR )
14 11 13 mp3an1 
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR )
15 14 adantl 
 |-  ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ A ) ) e. RR )
16 ovolun 
 |-  ( ( ( ( x i^i A ) C_ RR /\ ( vol* ` ( x i^i A ) ) e. RR ) /\ ( ( x \ A ) C_ RR /\ ( vol* ` ( x \ A ) ) e. RR ) ) -> ( vol* ` ( ( x i^i A ) u. ( x \ A ) ) ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) )
17 7 10 12 15 16 syl22anc 
 |-  ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( ( x i^i A ) u. ( x \ A ) ) ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) )
18 4 17 eqbrtrrid 
 |-  ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` x ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) )
19 simprr 
 |-  ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` x ) e. RR )
20 10 15 readdcld 
 |-  ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) e. RR )
21 19 20 letri3d 
 |-  ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <-> ( ( vol* ` x ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) /\ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) )
22 18 21 mpbirand 
 |-  ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <-> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) )
23 22 expr 
 |-  ( ( A C_ RR /\ x C_ RR ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <-> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) )
24 23 pm5.74d 
 |-  ( ( A C_ RR /\ x C_ RR ) -> ( ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) <-> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) )
25 2 24 sylan2 
 |-  ( ( A C_ RR /\ x e. ~P RR ) -> ( ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) <-> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) )
26 25 ralbidva 
 |-  ( A C_ RR -> ( A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) <-> A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) )
27 26 pm5.32i 
 |-  ( ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. 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 i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) )
28 1 27 bitri 
 |-  ( 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 ) ) ) )