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 φA
ovolshft.2 φC
ovolshft.3 φB=x|xCA
Assertion ovolshft φvol*A=vol*B

Proof

Step Hyp Ref Expression
1 ovolshft.1 φA
2 ovolshft.2 φC
3 ovolshft.3 φB=x|xCA
4 eqid z*|g2Bran.gz=supranseq1+absg*<=z*|g2Bran.gz=supranseq1+absg*<
5 1 2 3 4 ovolshftlem2 φy*|f2Aran.fy=supranseq1+absf*<z*|g2Bran.gz=supranseq1+absg*<
6 ssrab2 x|xCA
7 3 6 eqsstrdi φB
8 2 renegcld φC
9 1 2 3 shft2rab φA=w|wCB
10 eqid y*|f2Aran.fy=supranseq1+absf*<=y*|f2Aran.fy=supranseq1+absf*<
11 7 8 9 10 ovolshftlem2 φz*|g2Bran.gz=supranseq1+absg*<y*|f2Aran.fy=supranseq1+absf*<
12 5 11 eqssd φy*|f2Aran.fy=supranseq1+absf*<=z*|g2Bran.gz=supranseq1+absg*<
13 12 infeq1d φsupy*|f2Aran.fy=supranseq1+absf*<*<=supz*|g2Bran.gz=supranseq1+absg*<*<
14 10 ovolval Avol*A=supy*|f2Aran.fy=supranseq1+absf*<*<
15 1 14 syl φvol*A=supy*|f2Aran.fy=supranseq1+absf*<*<
16 4 ovolval Bvol*B=supz*|g2Bran.gz=supranseq1+absg*<*<
17 7 16 syl φvol*B=supz*|g2Bran.gz=supranseq1+absg*<*<
18 13 15 17 3eqtr4d φvol*A=vol*B