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 
|- ( ph -> A C_ RR )
ovolshft.2 
|- ( ph -> C e. RR )
ovolshft.3 
|- ( ph -> B = { x e. RR | ( x - C ) e. A } )
Assertion ovolshft 
|- ( ph -> ( vol* ` A ) = ( vol* ` B ) )

Proof

Step Hyp Ref Expression
1 ovolshft.1 
 |-  ( ph -> A C_ RR )
2 ovolshft.2 
 |-  ( ph -> C e. RR )
3 ovolshft.3 
 |-  ( ph -> B = { x e. RR | ( x - C ) e. A } )
4 eqid 
 |-  { z e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } = { z e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) }
5 1 2 3 4 ovolshftlem2 
 |-  ( ph -> { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } C_ { z e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } )
6 ssrab2 
 |-  { x e. RR | ( x - C ) e. A } C_ RR
7 3 6 eqsstrdi 
 |-  ( ph -> B C_ RR )
8 2 renegcld 
 |-  ( ph -> -u C e. RR )
9 1 2 3 shft2rab 
 |-  ( ph -> A = { w e. RR | ( w - -u C ) e. B } )
10 eqid 
 |-  { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
11 7 8 9 10 ovolshftlem2 
 |-  ( ph -> { z e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } C_ { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } )
12 5 11 eqssd 
 |-  ( ph -> { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } = { z e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } )
13 12 infeq1d 
 |-  ( ph -> inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) = inf ( { z e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } , RR* , < ) )
14 10 ovolval 
 |-  ( A C_ RR -> ( vol* ` A ) = inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) )
15 1 14 syl 
 |-  ( ph -> ( vol* ` A ) = inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) )
16 4 ovolval 
 |-  ( B C_ RR -> ( vol* ` B ) = inf ( { z e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } , RR* , < ) )
17 7 16 syl 
 |-  ( ph -> ( vol* ` B ) = inf ( { z e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } , RR* , < ) )
18 13 15 17 3eqtr4d 
 |-  ( ph -> ( vol* ` A ) = ( vol* ` B ) )