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* ‘ 𝐵 ) )