Metamath Proof Explorer

Theorem ovolshft

Description: The Lebesgue outer measure function is shift-invariant. (Contributed by Mario Carneiro, 22-Mar-2014) (Proof shortened by AV, 17-Sep-2020)

		Ref	Expression
	Hypotheses	ovolshft.1	$⊢ φ \to A \subseteq ℝ$
		ovolshft.2	$⊢ φ \to C \in ℝ$
		ovolshft.3	$⊢ φ \to B = \{x \in ℝ \| x - C \in A\}$
	Assertion	ovolshft	$⊢ φ \to {vol}^{} (A) = {vol}^{} (B)$

Proof

Step	Hyp	Ref	Expression
1		ovolshft.1	$⊢ φ \to A \subseteq ℝ$
2		ovolshft.2	$⊢ φ \to C \in ℝ$
3		ovolshft.3	$⊢ φ \to B = \{x \in ℝ \| x - C \in A\}$
4		eqid	$⊢ \{z \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} = \{z \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\}$
5	1 2 3 4	ovolshftlem2	$⊢ φ \to \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} \subseteq \{z \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\}$
6		ssrab2	$⊢ \{x \in ℝ \| x - C \in A\} \subseteq ℝ$
7	3 6	eqsstrdi	$⊢ φ \to B \subseteq ℝ$
8	2	renegcld	$⊢ φ \to - C \in ℝ$
9	1 2 3	shft2rab	$⊢ φ \to A = \{w \in ℝ \| w - (- C) \in B\}$
10		eqid	$⊢ \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
11	7 8 9 10	ovolshftlem2	$⊢ φ \to \{z \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} \subseteq \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
12	5 11	eqssd	$⊢ φ \to \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} = \{z \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\}$
13	12	infeq1d	$⊢ φ \to inf (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <) = inf (\{z \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} ℝ^{} <)$
14	10	ovolval	$⊢ A \subseteq ℝ \to {vol}^{} (A) = inf (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <)$
15	1 14	syl	$⊢ φ \to {vol}^{} (A) = inf (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <)$
16	4	ovolval	$⊢ B \subseteq ℝ \to {vol}^{} (B) = inf (\{z \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} ℝ^{} <)$
17	7 16	syl	$⊢ φ \to {vol}^{} (B) = inf (\{z \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} ℝ^{} <)$
18	13 15 17	3eqtr4d	$⊢ φ \to {vol}^{} (A) = {vol}^{} (B)$