Metamath Proof Explorer


Theorem unmbl

Description: A union of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Assertion unmbl
|- ( ( A e. dom vol /\ B e. dom vol ) -> ( A u. B ) e. dom vol )

Proof

Step Hyp Ref Expression
1 mblss
 |-  ( A e. dom vol -> A C_ RR )
2 mblss
 |-  ( B e. dom vol -> B C_ RR )
3 1 2 anim12i
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( A C_ RR /\ B C_ RR ) )
4 unss
 |-  ( ( A C_ RR /\ B C_ RR ) <-> ( A u. B ) C_ RR )
5 3 4 sylib
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( A u. B ) C_ RR )
6 elpwi
 |-  ( x e. ~P RR -> x C_ RR )
7 inss1
 |-  ( x i^i ( A u. B ) ) C_ x
8 ovolsscl
 |-  ( ( ( x i^i ( A u. B ) ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( A u. B ) ) ) e. RR )
9 7 8 mp3an1
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( A u. B ) ) ) e. RR )
10 9 adantl
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x i^i ( A u. B ) ) ) e. RR )
11 inss1
 |-  ( x i^i A ) C_ x
12 ovolsscl
 |-  ( ( ( x i^i A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR )
13 11 12 mp3an1
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR )
14 13 adantl
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x i^i A ) ) e. RR )
15 inss1
 |-  ( ( x \ A ) i^i B ) C_ ( x \ A )
16 difss
 |-  ( x \ A ) C_ x
17 simprl
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> x C_ RR )
18 16 17 sstrid
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( x \ A ) C_ RR )
19 ovolsscl
 |-  ( ( ( x \ A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR )
20 16 19 mp3an1
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR )
21 20 adantl
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ A ) ) e. RR )
22 ovolsscl
 |-  ( ( ( ( x \ A ) i^i B ) C_ ( x \ A ) /\ ( x \ A ) C_ RR /\ ( vol* ` ( x \ A ) ) e. RR ) -> ( vol* ` ( ( x \ A ) i^i B ) ) e. RR )
23 15 18 21 22 mp3an2i
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( ( x \ A ) i^i B ) ) e. RR )
24 14 23 readdcld
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) e. RR )
25 difss
 |-  ( x \ ( A u. B ) ) C_ x
26 ovolsscl
 |-  ( ( ( x \ ( A u. B ) ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ ( A u. B ) ) ) e. RR )
27 25 26 mp3an1
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ ( A u. B ) ) ) e. RR )
28 27 adantl
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ ( A u. B ) ) ) e. RR )
29 incom
 |-  ( ( x \ A ) i^i B ) = ( B i^i ( x \ A ) )
30 indifcom
 |-  ( B i^i ( x \ A ) ) = ( x i^i ( B \ A ) )
31 29 30 eqtri
 |-  ( ( x \ A ) i^i B ) = ( x i^i ( B \ A ) )
32 31 uneq2i
 |-  ( ( x i^i A ) u. ( ( x \ A ) i^i B ) ) = ( ( x i^i A ) u. ( x i^i ( B \ A ) ) )
33 indi
 |-  ( x i^i ( A u. ( B \ A ) ) ) = ( ( x i^i A ) u. ( x i^i ( B \ A ) ) )
34 undif2
 |-  ( A u. ( B \ A ) ) = ( A u. B )
35 34 ineq2i
 |-  ( x i^i ( A u. ( B \ A ) ) ) = ( x i^i ( A u. B ) )
36 32 33 35 3eqtr2ri
 |-  ( x i^i ( A u. B ) ) = ( ( x i^i A ) u. ( ( x \ A ) i^i B ) )
37 36 fveq2i
 |-  ( vol* ` ( x i^i ( A u. B ) ) ) = ( vol* ` ( ( x i^i A ) u. ( ( x \ A ) i^i B ) ) )
38 11 17 sstrid
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( x i^i A ) C_ RR )
39 15 18 sstrid
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( x \ A ) i^i B ) C_ RR )
40 ovolun
 |-  ( ( ( ( x i^i A ) C_ RR /\ ( vol* ` ( x i^i A ) ) e. RR ) /\ ( ( ( x \ A ) i^i B ) C_ RR /\ ( vol* ` ( ( x \ A ) i^i B ) ) e. RR ) ) -> ( vol* ` ( ( x i^i A ) u. ( ( x \ A ) i^i B ) ) ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) )
41 38 14 39 23 40 syl22anc
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( ( x i^i A ) u. ( ( x \ A ) i^i B ) ) ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) )
42 37 41 eqbrtrid
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x i^i ( A u. B ) ) ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) )
43 10 24 28 42 leadd1dd
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i ( A u. B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) <_ ( ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) )
44 simplr
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> B e. dom vol )
45 mblsplit
 |-  ( ( B e. dom vol /\ ( x \ A ) C_ RR /\ ( vol* ` ( x \ A ) ) e. RR ) -> ( vol* ` ( x \ A ) ) = ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( ( x \ A ) \ B ) ) ) )
46 44 18 21 45 syl3anc
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ A ) ) = ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( ( x \ A ) \ B ) ) ) )
47 difun1
 |-  ( x \ ( A u. B ) ) = ( ( x \ A ) \ B )
48 47 fveq2i
 |-  ( vol* ` ( x \ ( A u. B ) ) ) = ( vol* ` ( ( x \ A ) \ B ) )
49 48 oveq2i
 |-  ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) = ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( ( x \ A ) \ B ) ) )
50 46 49 eqtr4di
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ A ) ) = ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) )
51 50 oveq2d
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) = ( ( vol* ` ( x i^i A ) ) + ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) ) )
52 simpll
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> A e. dom vol )
53 simprr
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` x ) e. RR )
54 mblsplit
 |-  ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) )
55 52 17 53 54 syl3anc
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) )
56 14 recnd
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x i^i A ) ) e. CC )
57 23 recnd
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( ( x \ A ) i^i B ) ) e. CC )
58 28 recnd
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ ( A u. B ) ) ) e. CC )
59 56 57 58 addassd
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) = ( ( vol* ` ( x i^i A ) ) + ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) ) )
60 51 55 59 3eqtr4d
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` x ) = ( ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) )
61 43 60 breqtrrd
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i ( A u. B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) <_ ( vol* ` x ) )
62 61 expr
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ x C_ RR ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A u. B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) <_ ( vol* ` x ) ) )
63 6 62 sylan2
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ x e. ~P RR ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A u. B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) <_ ( vol* ` x ) ) )
64 63 ralrimiva
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A u. B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) <_ ( vol* ` x ) ) )
65 ismbl2
 |-  ( ( A u. B ) e. dom vol <-> ( ( A u. B ) C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A u. B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) <_ ( vol* ` x ) ) ) )
66 5 64 65 sylanbrc
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( A u. B ) e. dom vol )