Metamath Proof Explorer

Theorem nulmbl

Description: A nullset is measurable. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Assertion nulmbl ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) → 𝐴 ∈ dom vol )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) → 𝐴 ⊆ ℝ )
2 elpwi ⊢ ( 𝑥 ∈ 𝒫 ℝ → 𝑥 ⊆ ℝ )
3 inss2 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴
4 ovolssnul ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 ∧ 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) = 0 )
5 3 4 mp3an1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) = 0 )
6 5 adantr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) = 0 )
7 6 oveq1d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( 0 + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
8 difss ⊢ ( 𝑥 ∖ 𝐴 ) ⊆ 𝑥
9 ovolsscl ⊢ ( ( ( 𝑥 ∖ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ )
10 8 9 mp3an1 ⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ )
11 10 adantl ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ )
12 11 recnd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℂ )
13 12 addid2d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( 0 + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) )
14 7 13 eqtrd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) )
15 simprl ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → 𝑥 ⊆ ℝ )
16 ovolss ⊢ ( ( ( 𝑥 ∖ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ≤ ( vol* ‘ 𝑥 ) )
17 8 15 16 sylancr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ≤ ( vol* ‘ 𝑥 ) )
18 14 17 eqbrtrd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
19 18 expr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) ∧ 𝑥 ⊆ ℝ ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) )
20 2 19 sylan2 ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) ∧ 𝑥 ∈ 𝒫 ℝ ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) )
21 20 ralrimiva ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) → ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) )
22 ismbl2 ⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
23 1 21 22 sylanbrc ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) → 𝐴 ∈ dom vol )