cmmbl

Description: The complement of a measurable set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014)

		Ref	Expression
	Assertion	cmmbl	$⊢ A \in dom vol \to ℝ ∖ A \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		difssd	$⊢ A \in dom vol \to ℝ ∖ A \subseteq ℝ$
2		elpwi	$⊢ x \in 𝒫 ℝ \to x \subseteq ℝ$
3		inss1	$⊢ x \cap A \subseteq x$
4		ovolsscl	$⊢ (x \cap A \subseteq x \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap A) \in ℝ$
5	3 4	mp3an1	$⊢ (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap A) \in ℝ$
6	5	3adant1	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap A) \in ℝ$
7	6	recnd	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap A) \in ℂ$
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	3adant1	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ A) \in ℝ$
12	11	recnd	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ A) \in ℂ$
13	7 12	addcomd	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap A) + {vol}^{} (x ∖ A) = {vol}^{} (x ∖ A) + {vol}^{*} (x \cap A)$
14		mblsplit	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x) = {vol}^{} (x \cap A) + {vol}^{} (x ∖ A)$
15		indifcom	$⊢ ℝ \cap (x ∖ A) = x \cap (ℝ ∖ A)$
16		simp2	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to x \subseteq ℝ$
17	16	ssdifssd	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to x ∖ A \subseteq ℝ$
18		sseqin2	$⊢ x ∖ A \subseteq ℝ \leftrightarrow ℝ \cap (x ∖ A) = x ∖ A$
19	17 18	sylib	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to ℝ \cap (x ∖ A) = x ∖ A$
20	15 19	eqtr3id	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to x \cap (ℝ ∖ A) = x ∖ A$
21	20	fveq2d	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap (ℝ ∖ A)) = {vol}^{*} (x ∖ A)$
22		difin	$⊢ x ∖ (x \cap (ℝ ∖ A)) = x ∖ (ℝ ∖ A)$
23	20	difeq2d	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to x ∖ (x \cap (ℝ ∖ A)) = x ∖ (x ∖ A)$
24	22 23	eqtr3id	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to x ∖ (ℝ ∖ A) = x ∖ (x ∖ A)$
25		dfin4	$⊢ x \cap A = x ∖ (x ∖ A)$
26	24 25	eqtr4di	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to x ∖ (ℝ ∖ A) = x \cap A$
27	26	fveq2d	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ (ℝ ∖ A)) = {vol}^{*} (x \cap A)$
28	21 27	oveq12d	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap (ℝ ∖ A)) + {vol}^{} (x ∖ (ℝ ∖ A)) = {vol}^{} (x ∖ A) + {vol}^{*} (x \cap A)$
29	13 14 28	3eqtr4d	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x) = {vol}^{} (x \cap (ℝ ∖ A)) + {vol}^{} (x ∖ (ℝ ∖ A))$
30	29	3expia	$⊢ (A \in dom vol \land x \subseteq ℝ) \to ({vol}^{} (x) \in ℝ \to {vol}^{} (x) = {vol}^{} (x \cap (ℝ ∖ A)) + {vol}^{} (x ∖ (ℝ ∖ A)))$
31	2 30	sylan2	$⊢ (A \in dom vol \land x \in 𝒫 ℝ) \to ({vol}^{} (x) \in ℝ \to {vol}^{} (x) = {vol}^{} (x \cap (ℝ ∖ A)) + {vol}^{} (x ∖ (ℝ ∖ A)))$
32	31	ralrimiva	$⊢ A \in dom vol \to \forall x \in 𝒫 ℝ ({vol}^{} (x) \in ℝ \to {vol}^{} (x) = {vol}^{} (x \cap (ℝ ∖ A)) + {vol}^{} (x ∖ (ℝ ∖ A)))$
33		ismbl	$⊢ ℝ ∖ A \in dom vol \leftrightarrow (ℝ ∖ A \subseteq ℝ \land \forall x \in 𝒫 ℝ ({vol}^{} (x) \in ℝ \to {vol}^{} (x) = {vol}^{} (x \cap (ℝ ∖ A)) + {vol}^{} (x ∖ (ℝ ∖ A))))$
34	1 32 33	sylanbrc	$⊢ A \in dom vol \to ℝ ∖ A \in dom vol$

Metamath Proof Explorer

Theorem cmmbl

Proof