shftmbl

Description: A shift of a measurable set is measurable. (Contributed by Mario Carneiro, 22-Mar-2014)

		Ref	Expression
	Assertion	shftmbl	$⊢ (A \in dom vol \land B \in ℝ) \to \{x \in ℝ \| x - B \in A\} \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		ssrab2	$⊢ \{x \in ℝ \| x - B \in A\} \subseteq ℝ$
2	1	a1i	$⊢ (A \in dom vol \land B \in ℝ) \to \{x \in ℝ \| x - B \in A\} \subseteq ℝ$
3		elpwi	$⊢ y \in 𝒫 ℝ \to y \subseteq ℝ$
4		simpll	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to A \in dom vol$
5		ssrab2	$⊢ \{z \in ℝ \| z - (- B) \in y\} \subseteq ℝ$
6	5	a1i	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to \{z \in ℝ \| z - (- B) \in y\} \subseteq ℝ$
7		simprl	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to y \subseteq ℝ$
8		simplr	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to B \in ℝ$
9	8	renegcld	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to - B \in ℝ$
10		eqidd	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to \{z \in ℝ \| z - (- B) \in y\} = \{z \in ℝ \| z - (- B) \in y\}$
11	7 9 10	ovolshft	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{} (y) \in ℝ)) \to {vol}^{} (y) = {vol}^{*} (\{z \in ℝ \| z - (- B) \in y\})$
12		simprr	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{} (y) \in ℝ)) \to {vol}^{} (y) \in ℝ$
13	11 12	eqeltrrd	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{} (y) \in ℝ)) \to {vol}^{} (\{z \in ℝ \| z - (- B) \in y\}) \in ℝ$
14		mblsplit	$⊢ (A \in dom vol \land \{z \in ℝ \| z - (- B) \in y\} \subseteq ℝ \land {vol}^{} (\{z \in ℝ \| z - (- B) \in y\}) \in ℝ) \to {vol}^{} (\{z \in ℝ \| z - (- B) \in y\}) = {vol}^{} (\{z \in ℝ \| z - (- B) \in y\} \cap A) + {vol}^{} (\{z \in ℝ \| z - (- B) \in y\} ∖ A)$
15	4 6 13 14	syl3anc	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{} (y) \in ℝ)) \to {vol}^{} (\{z \in ℝ \| z - (- B) \in y\}) = {vol}^{} (\{z \in ℝ \| z - (- B) \in y\} \cap A) + {vol}^{} (\{z \in ℝ \| z - (- B) \in y\} ∖ A)$
16		inss1	$⊢ y \cap \{x \in ℝ \| x - B \in A\} \subseteq y$
17	16 7	sstrid	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to y \cap \{x \in ℝ \| x - B \in A\} \subseteq ℝ$
18		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
19	4 18	syl	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to A \subseteq ℝ$
20		eqidd	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to \{x \in ℝ \| x - B \in A\} = \{x \in ℝ \| x - B \in A\}$
21	19 8 20	shft2rab	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to A = \{z \in ℝ \| z - (- B) \in \{x \in ℝ \| x - B \in A\}\}$
22	21	ineq2d	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to \{z \in ℝ \| z - (- B) \in y\} \cap A = \{z \in ℝ \| z - (- B) \in y\} \cap \{z \in ℝ \| z - (- B) \in \{x \in ℝ \| x - B \in A\}\}$
23		inrab	$⊢ \{z \in ℝ \| z - (- B) \in y\} \cap \{z \in ℝ \| z - (- B) \in \{x \in ℝ \| x - B \in A\}\} = \{z \in ℝ \| (z - (- B) \in y \land z - (- B) \in \{x \in ℝ \| x - B \in A\})\}$
24		elin	$⊢ z - (- B) \in (y \cap \{x \in ℝ \| x - B \in A\}) \leftrightarrow (z - (- B) \in y \land z - (- B) \in \{x \in ℝ \| x - B \in A\})$
25	24	rabbii	$⊢ \{z \in ℝ \| z - (- B) \in (y \cap \{x \in ℝ \| x - B \in A\})\} = \{z \in ℝ \| (z - (- B) \in y \land z - (- B) \in \{x \in ℝ \| x - B \in A\})\}$
26	23 25	eqtr4i	$⊢ \{z \in ℝ \| z - (- B) \in y\} \cap \{z \in ℝ \| z - (- B) \in \{x \in ℝ \| x - B \in A\}\} = \{z \in ℝ \| z - (- B) \in (y \cap \{x \in ℝ \| x - B \in A\})\}$
27	22 26	eqtrdi	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to \{z \in ℝ \| z - (- B) \in y\} \cap A = \{z \in ℝ \| z - (- B) \in (y \cap \{x \in ℝ \| x - B \in A\})\}$
28	17 9 27	ovolshft	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{} (y) \in ℝ)) \to {vol}^{} (y \cap \{x \in ℝ \| x - B \in A\}) = {vol}^{*} (\{z \in ℝ \| z - (- B) \in y\} \cap A)$
29	7	ssdifssd	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to y ∖ \{x \in ℝ \| x - B \in A\} \subseteq ℝ$
30	21	difeq2d	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to \{z \in ℝ \| z - (- B) \in y\} ∖ A = \{z \in ℝ \| z - (- B) \in y\} ∖ \{z \in ℝ \| z - (- B) \in \{x \in ℝ \| x - B \in A\}\}$
31		difrab	$⊢ \{z \in ℝ \| z - (- B) \in y\} ∖ \{z \in ℝ \| z - (- B) \in \{x \in ℝ \| x - B \in A\}\} = \{z \in ℝ \| (z - (- B) \in y \land \neg z - (- B) \in \{x \in ℝ \| x - B \in A\})\}$
32		eldif	$⊢ z - (- B) \in (y ∖ \{x \in ℝ \| x - B \in A\}) \leftrightarrow (z - (- B) \in y \land \neg z - (- B) \in \{x \in ℝ \| x - B \in A\})$
33	32	rabbii	$⊢ \{z \in ℝ \| z - (- B) \in (y ∖ \{x \in ℝ \| x - B \in A\})\} = \{z \in ℝ \| (z - (- B) \in y \land \neg z - (- B) \in \{x \in ℝ \| x - B \in A\})\}$
34	31 33	eqtr4i	$⊢ \{z \in ℝ \| z - (- B) \in y\} ∖ \{z \in ℝ \| z - (- B) \in \{x \in ℝ \| x - B \in A\}\} = \{z \in ℝ \| z - (- B) \in (y ∖ \{x \in ℝ \| x - B \in A\})\}$
35	30 34	eqtrdi	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{*} (y) \in ℝ)) \to \{z \in ℝ \| z - (- B) \in y\} ∖ A = \{z \in ℝ \| z - (- B) \in (y ∖ \{x \in ℝ \| x - B \in A\})\}$
36	29 9 35	ovolshft	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{} (y) \in ℝ)) \to {vol}^{} (y ∖ \{x \in ℝ \| x - B \in A\}) = {vol}^{*} (\{z \in ℝ \| z - (- B) \in y\} ∖ A)$
37	28 36	oveq12d	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{} (y) \in ℝ)) \to {vol}^{} (y \cap \{x \in ℝ \| x - B \in A\}) + {vol}^{} (y ∖ \{x \in ℝ \| x - B \in A\}) = {vol}^{} (\{z \in ℝ \| z - (- B) \in y\} \cap A) + {vol}^{*} (\{z \in ℝ \| z - (- B) \in y\} ∖ A)$
38	15 11 37	3eqtr4d	$⊢ ((A \in dom vol \land B \in ℝ) \land (y \subseteq ℝ \land {vol}^{} (y) \in ℝ)) \to {vol}^{} (y) = {vol}^{} (y \cap \{x \in ℝ \| x - B \in A\}) + {vol}^{} (y ∖ \{x \in ℝ \| x - B \in A\})$
39	38	expr	$⊢ ((A \in dom vol \land B \in ℝ) \land y \subseteq ℝ) \to ({vol}^{} (y) \in ℝ \to {vol}^{} (y) = {vol}^{} (y \cap \{x \in ℝ \| x - B \in A\}) + {vol}^{} (y ∖ \{x \in ℝ \| x - B \in A\}))$
40	3 39	sylan2	$⊢ ((A \in dom vol \land B \in ℝ) \land y \in 𝒫 ℝ) \to ({vol}^{} (y) \in ℝ \to {vol}^{} (y) = {vol}^{} (y \cap \{x \in ℝ \| x - B \in A\}) + {vol}^{} (y ∖ \{x \in ℝ \| x - B \in A\}))$
41	40	ralrimiva	$⊢ (A \in dom vol \land B \in ℝ) \to \forall y \in 𝒫 ℝ ({vol}^{} (y) \in ℝ \to {vol}^{} (y) = {vol}^{} (y \cap \{x \in ℝ \| x - B \in A\}) + {vol}^{} (y ∖ \{x \in ℝ \| x - B \in A\}))$
42		ismbl	$⊢ \{x \in ℝ \| x - B \in A\} \in dom vol \leftrightarrow (\{x \in ℝ \| x - B \in A\} \subseteq ℝ \land \forall y \in 𝒫 ℝ ({vol}^{} (y) \in ℝ \to {vol}^{} (y) = {vol}^{} (y \cap \{x \in ℝ \| x - B \in A\}) + {vol}^{} (y ∖ \{x \in ℝ \| x - B \in A\})))$
43	2 41 42	sylanbrc	$⊢ (A \in dom vol \land B \in ℝ) \to \{x \in ℝ \| x - B \in A\} \in dom vol$

Metamath Proof Explorer

Theorem shftmbl

Proof