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 difexg 
 |-  ( A e. _V -> ( A \ B ) e. _V )
23 21 22 syl 
 |-  ( ph -> ( A \ B ) e. _V )
24 elpwg 
 |-  ( ( A \ B ) e. _V -> ( ( A \ B ) e. ~P RR <-> ( A \ B ) C_ RR ) )
25 23 24 syl 
 |-  ( ph -> ( ( A \ B ) e. ~P RR <-> ( A \ B ) C_ RR ) )
26 7 25 mpbird 
 |-  ( ph -> ( A \ B ) e. ~P RR )
27 ovolf 
 |-  vol* : ~P RR --> ( 0 [,] +oo )
28 27 ffvelrni 
 |-  ( ( A \ B ) e. ~P RR -> ( vol* ` ( A \ B ) ) e. ( 0 [,] +oo ) )
29 26 28 syl 
 |-  ( ph -> ( vol* ` ( A \ B ) ) e. ( 0 [,] +oo ) )
30 29 xrge0nemnfd 
 |-  ( ph -> ( vol* ` ( A \ B ) ) =/= -oo )
31 30 adantr 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) = +oo ) -> ( vol* ` ( A \ B ) ) =/= -oo )
32 xaddpnf2 
 |-  ( ( ( vol* ` ( A \ B ) ) e. RR* /\ ( vol* ` ( A \ B ) ) =/= -oo ) -> ( +oo +e ( vol* ` ( A \ B ) ) ) = +oo )
33 18 31 32 syl2anc 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) = +oo ) -> ( +oo +e ( vol* ` ( A \ B ) ) ) = +oo )
34 15 33 eqtr2d 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) = +oo ) -> +oo = ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
35 13 34 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 ) ) ) )
36 simpl 
 |-  ( ( ph /\ -. ( vol* ` ( A i^i B ) ) = +oo ) -> ph )
37 20 6 sselpwd 
 |-  ( ph -> ( A i^i B ) e. ~P RR )
38 27 ffvelrni 
 |-  ( ( A i^i B ) e. ~P RR -> ( vol* ` ( A i^i B ) ) e. ( 0 [,] +oo ) )
39 37 38 syl 
 |-  ( ph -> ( vol* ` ( A i^i B ) ) e. ( 0 [,] +oo ) )
40 39 adantr 
 |-  ( ( ph /\ -. ( vol* ` ( A i^i B ) ) = +oo ) -> ( vol* ` ( A i^i B ) ) e. ( 0 [,] +oo ) )
41 neqne 
 |-  ( -. ( vol* ` ( A i^i B ) ) = +oo -> ( vol* ` ( A i^i B ) ) =/= +oo )
42 41 adantl 
 |-  ( ( ph /\ -. ( vol* ` ( A i^i B ) ) = +oo ) -> ( vol* ` ( A i^i B ) ) =/= +oo )
43 ge0xrre 
 |-  ( ( ( vol* ` ( A i^i B ) ) e. ( 0 [,] +oo ) /\ ( vol* ` ( A i^i B ) ) =/= +oo ) -> ( vol* ` ( A i^i B ) ) e. RR )
44 40 42 43 syl2anc 
 |-  ( ( ph /\ -. ( vol* ` ( A i^i B ) ) = +oo ) -> ( vol* ` ( A i^i B ) ) e. RR )
45 12 adantr 
 |-  ( ( ph /\ ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ +oo )
46 oveq2 
 |-  ( ( vol* ` ( A \ B ) ) = +oo -> ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) = ( ( vol* ` ( A i^i B ) ) +e +oo ) )
47 46 adantl 
 |-  ( ( ph /\ ( vol* ` ( A \ B ) ) = +oo ) -> ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) = ( ( vol* ` ( A i^i B ) ) +e +oo ) )
48 ovolcl 
 |-  ( ( A i^i B ) C_ RR -> ( vol* ` ( A i^i B ) ) e. RR* )
49 6 48 syl 
 |-  ( ph -> ( vol* ` ( A i^i B ) ) e. RR* )
50 39 xrge0nemnfd 
 |-  ( ph -> ( vol* ` ( A i^i B ) ) =/= -oo )
51 xaddpnf1 
 |-  ( ( ( vol* ` ( A i^i B ) ) e. RR* /\ ( vol* ` ( A i^i B ) ) =/= -oo ) -> ( ( vol* ` ( A i^i B ) ) +e +oo ) = +oo )
52 49 50 51 syl2anc 
 |-  ( ph -> ( ( vol* ` ( A i^i B ) ) +e +oo ) = +oo )
53 52 adantr 
 |-  ( ( ph /\ ( vol* ` ( A \ B ) ) = +oo ) -> ( ( vol* ` ( A i^i B ) ) +e +oo ) = +oo )
54 47 53 eqtr2d 
 |-  ( ( ph /\ ( vol* ` ( A \ B ) ) = +oo ) -> +oo = ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
55 45 54 breqtrd 
 |-  ( ( ph /\ ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
56 55 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 ) ) ) )
57 simpll 
 |-  ( ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR ) /\ -. ( vol* ` ( A \ B ) ) = +oo ) -> ph )
58 simplr 
 |-  ( ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR ) /\ -. ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( A i^i B ) ) e. RR )
59 29 adantr 
 |-  ( ( ph /\ -. ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( A \ B ) ) e. ( 0 [,] +oo ) )
60 neqne 
 |-  ( -. ( vol* ` ( A \ B ) ) = +oo -> ( vol* ` ( A \ B ) ) =/= +oo )
61 60 adantl 
 |-  ( ( ph /\ -. ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( A \ B ) ) =/= +oo )
62 ge0xrre 
 |-  ( ( ( vol* ` ( A \ B ) ) e. ( 0 [,] +oo ) /\ ( vol* ` ( A \ B ) ) =/= +oo ) -> ( vol* ` ( A \ B ) ) e. RR )
63 59 61 62 syl2anc 
 |-  ( ( ph /\ -. ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( A \ B ) ) e. RR )
64 63 adantlr 
 |-  ( ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR ) /\ -. ( vol* ` ( A \ B ) ) = +oo ) -> ( vol* ` ( A \ B ) ) e. RR )
65 6 3ad2ant1 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( A i^i B ) C_ RR )
66 simp2 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( vol* ` ( A i^i B ) ) e. RR )
67 7 3ad2ant1 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( A \ B ) C_ RR )
68 simp3 
 |-  ( ( ph /\ ( vol* ` ( A i^i B ) ) e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( vol* ` ( A \ B ) ) e. RR )
69 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 ) ) ) )
70 65 66 67 68 69 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 ) ) ) )
71 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 ) ) ) )
72 71 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 ) ) ) )
73 72 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 ) ) ) )
74 70 73 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 ) ) ) )
75 57 58 64 74 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 ) ) ) )
76 56 75 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 ) ) ) )
77 36 44 76 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 ) ) ) )
78 35 77 pm2.61dan 
 |-  ( ph -> ( vol* ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
79 5 78 eqbrtrd 
 |-  ( ph -> ( vol* ` A ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )