Metamath Proof Explorer

Theorem ovolsplit

Description: The Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts, using addition for extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypothesis ovolsplit.1 
|- ( ph -> A C_ RR )
Assertion ovolsplit 
|- ( ph -> ( vol* ` A ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )

Proof

Step Hyp Ref Expression
1 ovolsplit.1 
 |-  ( ph -> A C_ RR )
2 inundif 
 |-  ( ( A i^i B ) u. ( A \ B ) ) = A
3 2 eqcomi 
 |-  A = ( ( A i^i B ) u. ( A \ B ) )
4 3 a1i 
 |-  ( ph -> A = ( ( A i^i B ) u. ( A \ B ) ) )
5 4 fveq2d 
 |-  ( ph -> ( vol* ` A ) = ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) )
6 1 ssinss1d 
 |-  ( ph -> ( A i^i B ) C_ RR )
7 1 ssdifssd 
 |-  ( ph -> ( A \ B ) C_ RR )
8 6 7 unssd 
 |-  ( ph -> ( ( A i^i B ) u. ( A \ B ) ) C_ RR )
9 ovolcl 
 |-  ( ( ( A i^i B ) u. ( A \ B ) ) C_ RR -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) e. RR* )
10 8 9 syl 
 |-  ( ph -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) e. RR* )
11 pnfge 
 |-  ( ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) e. RR* -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ +oo )
12 10 11 syl 
 |-  ( ph -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ +oo )
13 12 adantr 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) = +oo ) -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ +oo )
14 oveq1 
 |-  ( ( vol* ` ( A i^i B ) ) = +oo -> ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) = ( +oo +e ( vol* ` ( A \ B ) ) ) )
15 14 adantl 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) = +oo ) -> ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) = ( +oo +e ( vol* ` ( A \ B ) ) ) )
16 ovolcl 
 |-  ( ( A \ B ) C_ RR -> ( vol* ` ( A \ B ) ) e. RR* )
17 7 16 syl 
 |-  ( ph -> ( vol* ` ( A \ B ) ) e. RR* )
18 17 adantr 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) = +oo ) -> ( vol* ` ( A \ B ) ) e. RR* )
19 reex 
 |-  RR e. _V
20 19 a1i 
 |-  ( ph -> RR e. _V )
21 20 1 ssexd 
 |-  ( ph -> A e. _V )
22 21 difexd 
 |-  ( ph -> ( A \ B ) e. _V )
23 elpwg 
 |-  ( ( A \ B ) e. _V -> ( ( A \ B ) e. ~P RR <-> ( A \ B ) C_ RR ) )
24 22 23 syl 
 |-  ( ph -> ( ( A \ B ) e. ~P RR <-> ( A \ B ) C_ RR ) )
25 7 24 mpbird 
 |-  ( ph -> ( A \ B ) e. ~P RR )
26 ovolf 
 |-  vol* : ~P RR --> ( 0 [,] +oo )
27 26 ffvelrni 
 |-  ( ( A \ B ) e. ~P RR -> ( vol* ` ( A \ B ) ) e. ( 0 [,] +oo ) )
28 25 27 syl 
 |-  ( ph -> ( vol* ` ( A \ B ) ) e. ( 0 [,] +oo ) )
29 28 xrge0nemnfd 
 |-  ( ph -> ( vol* ` ( A \ B ) ) =/= -oo )
30 29 adantr 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) = +oo ) -> ( vol* ` ( A \ B ) ) =/= -oo )
31 xaddpnf2 
 |-  ( ( ( vol* ` ( A \ B ) ) e. RR* /\ ( vol* ` ( A \ B ) ) =/= -oo ) -> ( +oo +e ( vol* ` ( A \ B ) ) ) = +oo )
32 18 30 31 syl2anc 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) = +oo ) -> ( +oo +e ( vol* ` ( A \ B ) ) ) = +oo )
33 15 32 eqtr2d 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) = +oo ) -> +oo = ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
34 13 33 breqtrd 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) = +oo ) -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
35 simpl 
 |-  ( ( ph /\ -. ( vol* ` ( A i^i B ) ) = +oo ) -> ph )
36 20 6 sselpwd 
 |-  ( ph -> ( A i^i B ) e. ~P RR )
37 26 ffvelrni 
 |-  ( ( A i^i B ) e. ~P RR -> ( vol* ` ( A i^i B ) ) e. ( 0 [,] +oo ) )
38 36 37 syl 
 |-  ( ph -> ( vol* ` ( A i^i B ) ) e. ( 0 [,] +oo ) )
39 38 adantr 
 |-  ( ( ph /\ -. ( vol* ` ( A i^i B ) ) = +oo ) -> ( vol* ` ( A i^i B ) ) e. ( 0 [,] +oo ) )
40 neqne 
 |-  ( -. ( vol* ` ( A i^i B ) ) = +oo -> ( vol* ` ( A i^i B ) ) =/= +oo )
41 40 adantl 
 |-  ( ( ph /\ -. ( vol* ` ( A i^i B ) ) = +oo ) -> ( vol* ` ( A i^i B ) ) =/= +oo )
42 ge0xrre 
 |-  ( ( ( vol* ` ( A i^i B ) ) e. ( 0 [,] +oo ) /\ ( vol* ` ( A i^i B ) ) =/= +oo ) -> ( vol* ` ( A i^i B ) ) e. RR )
43 39 41 42 syl2anc 
 |-  ( ( ph /\ -. ( vol* ` ( A i^i B ) ) = +oo ) -> ( vol* ` ( A i^i B ) ) e. RR )
44 12 adantr 
 |-  ( ( ph /\ ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ +oo )
45 oveq2 
 |-  ( ( vol* ` ( A \ B ) ) = +oo -> ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) = ( ( vol* ` ( A i^i B ) ) +e +oo ) )
46 45 adantl 
 |-  ( ( ph /\ ( vol* ` ( A \ B ) ) = +oo ) -> ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) = ( ( vol* ` ( A i^i B ) ) +e +oo ) )
47 ovolcl 
 |-  ( ( A i^i B ) C_ RR -> ( vol* ` ( A i^i B ) ) e. RR* )
48 6 47 syl 
 |-  ( ph -> ( vol* ` ( A i^i B ) ) e. RR* )
49 38 xrge0nemnfd 
 |-  ( ph -> ( vol* ` ( A i^i B ) ) =/= -oo )
50 xaddpnf1 
 |-  ( ( ( vol* ` ( A i^i B ) ) e. RR* /\ ( vol* ` ( A i^i B ) ) =/= -oo ) -> ( ( vol* ` ( A i^i B ) ) +e +oo ) = +oo )
51 48 49 50 syl2anc 
 |-  ( ph -> ( ( vol* ` ( A i^i B ) ) +e +oo ) = +oo )
52 51 adantr 
 |-  ( ( ph /\ ( vol* ` ( A \ B ) ) = +oo ) -> ( ( vol* ` ( A i^i B ) ) +e +oo ) = +oo )
53 46 52 eqtr2d 
 |-  ( ( ph /\ ( vol* ` ( A \ B ) ) = +oo ) -> +oo = ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
54 44 53 breqtrd 
 |-  ( ( ph /\ ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
55 54 adantlr 
 |-  ( ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR ) /\ ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
56 simpll 
 |-  ( ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR ) /\ -. ( vol* ` ( A \ B ) ) = +oo ) -> ph )
57 simplr 
 |-  ( ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR ) /\ -. ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( A i^i B ) ) e. RR )
58 28 adantr 
 |-  ( ( ph /\ -. ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( A \ B ) ) e. ( 0 [,] +oo ) )
59 neqne 
 |-  ( -. ( vol* ` ( A \ B ) ) = +oo -> ( vol* ` ( A \ B ) ) =/= +oo )
60 59 adantl 
 |-  ( ( ph /\ -. ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( A \ B ) ) =/= +oo )
61 ge0xrre 
 |-  ( ( ( vol* ` ( A \ B ) ) e. ( 0 [,] +oo ) /\ ( vol* ` ( A \ B ) ) =/= +oo ) -> ( vol* ` ( A \ B ) ) e. RR )
62 58 60 61 syl2anc 
 |-  ( ( ph /\ -. ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( A \ B ) ) e. RR )
63 62 adantlr 
 |-  ( ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR ) /\ -. ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( A \ B ) ) e. RR )
64 6 3ad2ant1 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( A i^i B ) C_ RR )
65 simp2 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( vol* ` ( A i^i B ) ) e. RR )
66 7 3ad2ant1 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( A \ B ) C_ RR )
67 simp3 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( vol* ` ( A \ B ) ) e. RR )
68 ovolun 
 |-  ( ( ( ( A i^i B ) C_ RR /\ ( vol* ` ( A i^i B ) ) e. RR ) /\ ( ( A \ B ) C_ RR /\ ( vol* ` ( A \ B ) ) e. RR ) ) -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ ( ( vol* ` ( A i^i B ) ) + ( vol* ` ( A \ B ) ) ) )
69 64 65 66 67 68 syl22anc 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ ( ( vol* ` ( A i^i B ) ) + ( vol* ` ( A \ B ) ) ) )
70 rexadd 
 |-  ( ( ( vol* ` ( A i^i B ) ) e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) = ( ( vol* ` ( A i^i B ) ) + ( vol* ` ( A \ B ) ) ) )
71 70 eqcomd 
 |-  ( ( ( vol* ` ( A i^i B ) ) e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( ( vol* ` ( A i^i B ) ) + ( vol* ` ( A \ B ) ) ) = ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
72 71 3adant1 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( ( vol* ` ( A i^i B ) ) + ( vol* ` ( A \ B ) ) ) = ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
73 69 72 breqtrd 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
74 56 57 63 73 syl3anc 
 |-  ( ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR ) /\ -. ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
75 55 74 pm2.61dan 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR ) -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
76 35 43 75 syl2anc 
 |-  ( ( ph /\ -. ( vol* ` ( A i^i B ) ) = +oo ) -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
77 34 76 pm2.61dan 
 |-  ( ph -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
78 5 77 eqbrtrd 
 |-  ( ph -> ( vol* ` A ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )