Metamath Proof Explorer

Theorem ovolunnul

Description: Adding a nullset does not change the measure of a set. (Contributed by Mario Carneiro, 25-Mar-2015)

Ref Expression
Assertion ovolunnul 
|- ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( vol* ` ( A u. B ) ) = ( vol* ` A ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> A C_ RR )
2 simp2 
 |-  ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> B C_ RR )
3 1 2 unssd 
 |-  ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( A u. B ) C_ RR )
4 ovolcl 
 |-  ( ( A u. B ) C_ RR -> ( vol* ` ( A u. B ) ) e. RR* )
5 3 4 syl 
 |-  ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( vol* ` ( A u. B ) ) e. RR* )
6 ovolcl 
 |-  ( A C_ RR -> ( vol* ` A ) e. RR* )
7 6 3ad2ant1 
 |-  ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( vol* ` A ) e. RR* )
8 xrltnle 
 |-  ( ( ( vol* ` A ) e. RR* /\ ( vol* ` ( A u. B ) ) e. RR* ) -> ( ( vol* ` A ) < ( vol* ` ( A u. B ) ) <-> -. ( vol* ` ( A u. B ) ) <_ ( vol* ` A ) ) )
9 7 5 8 syl2anc 
 |-  ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( ( vol* ` A ) < ( vol* ` ( A u. B ) ) <-> -. ( vol* ` ( A u. B ) ) <_ ( vol* ` A ) ) )
10 1 adantr 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> A C_ RR )
11 mnfxr 
 |-  -oo e. RR*
12 11 a1i 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> -oo e. RR* )
13 10 6 syl 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> ( vol* ` A ) e. RR* )
14 5 adantr 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> ( vol* ` ( A u. B ) ) e. RR* )
15 ovolge0 
 |-  ( A C_ RR -> 0 <_ ( vol* ` A ) )
16 15 3ad2ant1 
 |-  ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> 0 <_ ( vol* ` A ) )
17 ge0gtmnf 
 |-  ( ( ( vol* ` A ) e. RR* /\ 0 <_ ( vol* ` A ) ) -> -oo < ( vol* ` A ) )
18 7 16 17 syl2anc 
 |-  ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> -oo < ( vol* ` A ) )
19 18 adantr 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> -oo < ( vol* ` A ) )
20 simpr 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> ( vol* ` A ) < ( vol* ` ( A u. B ) ) )
21 xrre2 
 |-  ( ( ( -oo e. RR* /\ ( vol* ` A ) e. RR* /\ ( vol* ` ( A u. B ) ) e. RR* ) /\ ( -oo < ( vol* ` A ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) ) -> ( vol* ` A ) e. RR )
22 12 13 14 19 20 21 syl32anc 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> ( vol* ` A ) e. RR )
23 2 adantr 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> B C_ RR )
24 simpl3 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> ( vol* ` B ) = 0 )
25 0re 
 |-  0 e. RR
26 24 25 eqeltrdi 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> ( vol* ` B ) e. RR )
27 ovolun 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) <_ ( ( vol* ` A ) + ( vol* ` B ) ) )
28 10 22 23 26 27 syl22anc 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> ( vol* ` ( A u. B ) ) <_ ( ( vol* ` A ) + ( vol* ` B ) ) )
29 24 oveq2d 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> ( ( vol* ` A ) + ( vol* ` B ) ) = ( ( vol* ` A ) + 0 ) )
30 22 recnd 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> ( vol* ` A ) e. CC )
31 30 addid1d 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> ( ( vol* ` A ) + 0 ) = ( vol* ` A ) )
32 29 31 eqtrd 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> ( ( vol* ` A ) + ( vol* ` B ) ) = ( vol* ` A ) )
33 28 32 breqtrd 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) /\ ( vol* ` A ) < ( vol* ` ( A u. B ) ) ) -> ( vol* ` ( A u. B ) ) <_ ( vol* ` A ) )
34 33 ex 
 |-  ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( ( vol* ` A ) < ( vol* ` ( A u. B ) ) -> ( vol* ` ( A u. B ) ) <_ ( vol* ` A ) ) )
35 9 34 sylbird 
 |-  ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( -. ( vol* ` ( A u. B ) ) <_ ( vol* ` A ) -> ( vol* ` ( A u. B ) ) <_ ( vol* ` A ) ) )
36 35 pm2.18d 
 |-  ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( vol* ` ( A u. B ) ) <_ ( vol* ` A ) )
37 ssun1 
 |-  A C_ ( A u. B )
38 ovolss 
 |-  ( ( A C_ ( A u. B ) /\ ( A u. B ) C_ RR ) -> ( vol* ` A ) <_ ( vol* ` ( A u. B ) ) )
39 37 3 38 sylancr 
 |-  ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( vol* ` A ) <_ ( vol* ` ( A u. B ) ) )
40 5 7 36 39 xrletrid 
 |-  ( ( A C_ RR /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( vol* ` ( A u. B ) ) = ( vol* ` A ) )