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 )