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 ) ) ) )