This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
ovolshft.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
ovolshft.3 ⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
Assertion ovolshft ( 𝜑 → ( vol* ‘ 𝐴 ) = ( vol* ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ovolshft.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 ovolshft.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3 ovolshft.3 ⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
4 eqid ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) }
5 1 2 3 4 ovolshftlem2 ⊢ ( 𝜑 → { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } ⊆ { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } )
6 ssrab2 ⊢ { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } ⊆ ℝ
7 3 6 eqsstrdi ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
8 2 renegcld ⊢ ( 𝜑 → - 𝐶 ∈ ℝ )
9 1 2 3 shft2rab ⊢ ( 𝜑 → 𝐴 = { 𝑤 ∈ ℝ ∣ ( 𝑤 − - 𝐶 ) ∈ 𝐵 } )
10 eqid ⊢ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
11 7 8 9 10 ovolshftlem2 ⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } ⊆ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } )
12 5 11 eqssd ⊢ ( 𝜑 → { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } )
13 12 infeq1d ⊢ ( 𝜑 → inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } , ℝ* , < ) = inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } , ℝ* , < ) )
14 10 ovolval ⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) = inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } , ℝ* , < ) )
15 1 14 syl ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } , ℝ* , < ) )
16 4 ovolval ⊢ ( 𝐵 ⊆ ℝ → ( vol* ‘ 𝐵 ) = inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } , ℝ* , < ) )
17 7 16 syl ⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) = inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } , ℝ* , < ) )
18 13 15 17 3eqtr4d ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = ( vol* ‘ 𝐵 ) )