nulmbl

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

		Ref	Expression
	Assertion	nulmbl	$⊢ (A \subseteq ℝ \land {vol}^{*} (A) = 0) \to A \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \subseteq ℝ \land {vol}^{*} (A) = 0) \to A \subseteq ℝ$
2		elpwi	$⊢ x \in 𝒫 ℝ \to x \subseteq ℝ$
3		inss2	$⊢ x \cap A \subseteq A$
4		ovolssnul	$⊢ (x \cap A \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) = 0) \to {vol}^{} (x \cap A) = 0$
5	3 4	mp3an1	$⊢ (A \subseteq ℝ \land {vol}^{} (A) = 0) \to {vol}^{} (x \cap A) = 0$
6	5	adantr	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) = 0) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{*} (x \cap A) = 0$
7	6	oveq1d	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) = 0) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap A) + {vol}^{} (x ∖ A) = 0 + {vol}^{*} (x ∖ A)$
8		difss	$⊢ x ∖ A \subseteq x$
9		ovolsscl	$⊢ (x ∖ A \subseteq x \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ A) \in ℝ$
10	8 9	mp3an1	$⊢ (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ A) \in ℝ$
11	10	adantl	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) = 0) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{*} (x ∖ A) \in ℝ$
12	11	recnd	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) = 0) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{*} (x ∖ A) \in ℂ$
13	12	addlidd	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) = 0) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to 0 + {vol}^{} (x ∖ A) = {vol}^{} (x ∖ A)$
14	7 13	eqtrd	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) = 0) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap A) + {vol}^{} (x ∖ A) = {vol}^{*} (x ∖ A)$
15		simprl	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) = 0) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to x \subseteq ℝ$
16		ovolss	$⊢ (x ∖ A \subseteq x \land x \subseteq ℝ) \to {vol}^{} (x ∖ A) \leq {vol}^{} (x)$
17	8 15 16	sylancr	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) = 0) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x ∖ A) \leq {vol}^{} (x)$
18	14 17	eqbrtrd	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) = 0) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap A) + {vol}^{} (x ∖ A) \leq {vol}^{*} (x)$
19	18	expr	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) = 0) \land x \subseteq ℝ) \to ({vol}^{} (x) \in ℝ \to {vol}^{} (x \cap A) + {vol}^{} (x ∖ A) \leq {vol}^{*} (x))$
20	2 19	sylan2	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) = 0) \land x \in 𝒫 ℝ) \to ({vol}^{} (x) \in ℝ \to {vol}^{} (x \cap A) + {vol}^{} (x ∖ A) \leq {vol}^{*} (x))$
21	20	ralrimiva	$⊢ (A \subseteq ℝ \land {vol}^{} (A) = 0) \to \forall x \in 𝒫 ℝ ({vol}^{} (x) \in ℝ \to {vol}^{} (x \cap A) + {vol}^{} (x ∖ A) \leq {vol}^{*} (x))$
22		ismbl2	$⊢ A \in dom vol \leftrightarrow (A \subseteq ℝ \land \forall x \in 𝒫 ℝ ({vol}^{} (x) \in ℝ \to {vol}^{} (x \cap A) + {vol}^{} (x ∖ A) \leq {vol}^{} (x)))$
23	1 21 22	sylanbrc	$⊢ (A \subseteq ℝ \land {vol}^{*} (A) = 0) \to A \in dom vol$

Metamath Proof Explorer

Theorem nulmbl

Proof