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 ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) = ( vol* ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → 𝐴 ⊆ ℝ )
2 simp2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → 𝐵 ⊆ ℝ )
3 1 2 unssd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( 𝐴 ∪ 𝐵 ) ⊆ ℝ )
4 ovolcl ⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ℝ → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ℝ* )
5 3 4 syl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ℝ* )
6 ovolcl ⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) ∈ ℝ* )
7 6 3ad2ant1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( vol* ‘ 𝐴 ) ∈ ℝ* )
8 xrltnle ⊢ ( ( ( vol* ‘ 𝐴 ) ∈ ℝ* ∧ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ℝ* ) → ( ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ ¬ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( vol* ‘ 𝐴 ) ) )
9 7 5 8 syl2anc ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ ¬ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( vol* ‘ 𝐴 ) ) )
10 1 adantr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → 𝐴 ⊆ ℝ )
11 mnfxr ⊢ -∞ ∈ ℝ*
12 11 a1i ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → -∞ ∈ ℝ* )
13 10 6 syl ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( vol* ‘ 𝐴 ) ∈ ℝ* )
14 5 adantr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ℝ* )
15 ovolge0 ⊢ ( 𝐴 ⊆ ℝ → 0 ≤ ( vol* ‘ 𝐴 ) )
16 15 3ad2ant1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → 0 ≤ ( vol* ‘ 𝐴 ) )
17 ge0gtmnf ⊢ ( ( ( vol* ‘ 𝐴 ) ∈ ℝ* ∧ 0 ≤ ( vol* ‘ 𝐴 ) ) → -∞ < ( vol* ‘ 𝐴 ) )
18 7 16 17 syl2anc ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → -∞ < ( vol* ‘ 𝐴 ) )
19 18 adantr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → -∞ < ( vol* ‘ 𝐴 ) )
20 simpr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) )
21 xrre2 ⊢ ( ( ( -∞ ∈ ℝ* ∧ ( vol* ‘ 𝐴 ) ∈ ℝ* ∧ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ℝ* ) ∧ ( -∞ < ( vol* ‘ 𝐴 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
22 12 13 14 19 20 21 syl32anc ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
23 2 adantr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → 𝐵 ⊆ ℝ )
24 simpl3 ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( vol* ‘ 𝐵 ) = 0 )
25 0re ⊢ 0 ∈ ℝ
26 24 25 eqeltrdi ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( vol* ‘ 𝐵 ) ∈ ℝ )
27 ovolun ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) )
28 10 22 23 26 27 syl22anc ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) )
29 24 oveq2d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) = ( ( vol* ‘ 𝐴 ) + 0 ) )
30 22 recnd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( vol* ‘ 𝐴 ) ∈ ℂ )
31 30 addid1d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( ( vol* ‘ 𝐴 ) + 0 ) = ( vol* ‘ 𝐴 ) )
32 29 31 eqtrd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) = ( vol* ‘ 𝐴 ) )
33 28 32 breqtrd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) ∧ ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( vol* ‘ 𝐴 ) )
34 33 ex ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( ( vol* ‘ 𝐴 ) < ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( vol* ‘ 𝐴 ) ) )
35 9 34 sylbird ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( ¬ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( vol* ‘ 𝐴 ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( vol* ‘ 𝐴 ) ) )
36 35 pm2.18d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( vol* ‘ 𝐴 ) )
37 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
38 ovolss ⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ℝ ) → ( vol* ‘ 𝐴 ) ≤ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) )
39 37 3 38 sylancr ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( vol* ‘ 𝐴 ) ≤ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) )
40 5 7 36 39 xrletrid ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) = ( vol* ‘ 𝐴 ) )