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 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
Assertion ovolsplit ( 𝜑 → ( vol* ‘ 𝐴 ) ≤ ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 ovolsplit.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 inundif ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴
3 2 eqcomi ⊢ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) )
4 3 a1i ⊢ ( 𝜑 → 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) )
5 4 fveq2d ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) )
6 1 ssinss1d ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ ℝ )
7 1 ssdifssd ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ ℝ )
8 6 7 unssd ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ⊆ ℝ )
9 ovolcl ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ⊆ ℝ → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ∈ ℝ* )
10 8 9 syl ⊢ ( 𝜑 → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ∈ ℝ* )
11 pnfge ⊢ ( ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ∈ ℝ* → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ +∞ )
12 10 11 syl ⊢ ( 𝜑 → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ +∞ )
13 12 adantr ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ +∞ )
14 oveq1 ⊢ ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ → ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( +∞ +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ ) → ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( +∞ +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
16 ovolcl ⊢ ( ( 𝐴 ∖ 𝐵 ) ⊆ ℝ → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ* )
17 7 16 syl ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ* )
18 17 adantr ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ* )
19 reex ⊢ ℝ ∈ V
20 19 a1i ⊢ ( 𝜑 → ℝ ∈ V )
21 20 1 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
22 21 difexd ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ∈ V )
23 elpwg ⊢ ( ( 𝐴 ∖ 𝐵 ) ∈ V → ( ( 𝐴 ∖ 𝐵 ) ∈ 𝒫 ℝ ↔ ( 𝐴 ∖ 𝐵 ) ⊆ ℝ ) )
24 22 23 syl ⊢ ( 𝜑 → ( ( 𝐴 ∖ 𝐵 ) ∈ 𝒫 ℝ ↔ ( 𝐴 ∖ 𝐵 ) ⊆ ℝ ) )
25 7 24 mpbird ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ∈ 𝒫 ℝ )
26 ovolf ⊢ vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ )
27 26 ffvelcdmi ⊢ ( ( 𝐴 ∖ 𝐵 ) ∈ 𝒫 ℝ → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
28 25 27 syl ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
29 28 xrge0nemnfd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ≠ -∞ )
30 29 adantr ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ≠ -∞ )
31 xaddpnf2 ⊢ ( ( ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ* ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ≠ -∞ ) → ( +∞ +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) = +∞ )
32 18 30 31 syl2anc ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ ) → ( +∞ +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) = +∞ )
33 15 32 eqtr2d ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ ) → +∞ = ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
34 13 33 breqtrd ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
35 simpl ⊢ ( ( 𝜑 ∧ ¬ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ ) → 𝜑 )
36 20 6 sselpwd ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ 𝒫 ℝ )
37 26 ffvelcdmi ⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝒫 ℝ → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
38 36 37 syl ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ ¬ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
40 neqne ⊢ ( ¬ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ≠ +∞ )
41 40 adantl ⊢ ( ( 𝜑 ∧ ¬ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ≠ +∞ )
42 ge0xrre ⊢ ( ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ( 0 [,] +∞ ) ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ≠ +∞ ) → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ )
43 39 41 42 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ )
44 12 adantr ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ +∞ )
45 oveq2 ⊢ ( ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ → ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 +∞ ) )
46 45 adantl ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ ) → ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 +∞ ) )
47 ovolcl ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ ℝ → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ* )
48 6 47 syl ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ* )
49 38 xrge0nemnfd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ≠ -∞ )
50 xaddpnf1 ⊢ ( ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ* ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ≠ -∞ ) → ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 +∞ ) = +∞ )
51 48 49 50 syl2anc ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 +∞ ) = +∞ )
52 51 adantr ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ ) → ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 +∞ ) = +∞ )
53 46 52 eqtr2d ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ ) → +∞ = ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
54 44 53 breqtrd ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
55 54 adantlr ⊢ ( ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ) ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
56 simpll ⊢ ( ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ) ∧ ¬ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ ) → 𝜑 )
57 simplr ⊢ ( ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ) ∧ ¬ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ )
58 28 adantr ⊢ ( ( 𝜑 ∧ ¬ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
59 neqne ⊢ ( ¬ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ≠ +∞ )
60 59 adantl ⊢ ( ( 𝜑 ∧ ¬ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ≠ +∞ )
61 ge0xrre ⊢ ( ( ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ( 0 [,] +∞ ) ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ≠ +∞ ) → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ )
62 58 60 61 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ )
63 62 adantlr ⊢ ( ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ) ∧ ¬ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ )
64 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ ) → ( 𝐴 ∩ 𝐵 ) ⊆ ℝ )
65 simp2 ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ )
66 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ ) → ( 𝐴 ∖ 𝐵 ) ⊆ ℝ )
67 simp3 ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ )
68 ovolun ⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ) ∧ ( ( 𝐴 ∖ 𝐵 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
69 64 65 66 67 68 syl22anc ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
70 rexadd ⊢ ( ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ ) → ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
71 70 eqcomd ⊢ ( ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ ) → ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
72 71 3adant1 ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ ) → ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
73 69 72 breqtrd ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ∧ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
74 56 57 63 73 syl3anc ⊢ ( ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ) ∧ ¬ ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
75 55 74 pm2.61dan ⊢ ( ( 𝜑 ∧ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
76 35 43 75 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = +∞ ) → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
77 34 76 pm2.61dan ⊢ ( 𝜑 → ( vol* ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
78 5 77 eqbrtrd ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) ≤ ( ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ) )