Metamath Proof Explorer

Theorem ovolshftlem2

Description: Lemma for ovolshft . (Contributed by Mario Carneiro, 22-Mar-2014)

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 } )
ovolshft.4 
|- M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
Assertion ovolshftlem2 
|- ( ph -> { z e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } C_ M )

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 ovolshft.4 
 |-  M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
5 1 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. RR* ) /\ g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ A C_ U. ran ( (,) o. g ) ) -> A C_ RR )
6 2 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. RR* ) /\ g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ A C_ U. ran ( (,) o. g ) ) -> C e. RR )
7 3 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. RR* ) /\ g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ A C_ U. ran ( (,) o. g ) ) -> B = { x e. RR | ( x - C ) e. A } )
8 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. g ) ) = seq 1 ( + , ( ( abs o. - ) o. g ) )
9 2fveq3 
 |-  ( m = n -> ( 1st ` ( g ` m ) ) = ( 1st ` ( g ` n ) ) )
10 9 oveq1d 
 |-  ( m = n -> ( ( 1st ` ( g ` m ) ) + C ) = ( ( 1st ` ( g ` n ) ) + C ) )
11 2fveq3 
 |-  ( m = n -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` n ) ) )
12 11 oveq1d 
 |-  ( m = n -> ( ( 2nd ` ( g ` m ) ) + C ) = ( ( 2nd ` ( g ` n ) ) + C ) )
13 10 12 opeq12d 
 |-  ( m = n -> <. ( ( 1st ` ( g ` m ) ) + C ) , ( ( 2nd ` ( g ` m ) ) + C ) >. = <. ( ( 1st ` ( g ` n ) ) + C ) , ( ( 2nd ` ( g ` n ) ) + C ) >. )
14 13 cbvmptv 
 |-  ( m e. NN |-> <. ( ( 1st ` ( g ` m ) ) + C ) , ( ( 2nd ` ( g ` m ) ) + C ) >. ) = ( n e. NN |-> <. ( ( 1st ` ( g ` n ) ) + C ) , ( ( 2nd ` ( g ` n ) ) + C ) >. )
15 simplr 
 |-  ( ( ( ( ph /\ z e. RR* ) /\ g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ A C_ U. ran ( (,) o. g ) ) -> g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
16 elovolmlem 
 |-  ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> g : NN --> ( <_ i^i ( RR X. RR ) ) )
17 15 16 sylib 
 |-  ( ( ( ( ph /\ z e. RR* ) /\ g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ A C_ U. ran ( (,) o. g ) ) -> g : NN --> ( <_ i^i ( RR X. RR ) ) )
18 simpr 
 |-  ( ( ( ( ph /\ z e. RR* ) /\ g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ A C_ U. ran ( (,) o. g ) ) -> A C_ U. ran ( (,) o. g ) )
19 5 6 7 4 8 14 17 18 ovolshftlem1 
 |-  ( ( ( ( ph /\ z e. RR* ) /\ g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ A C_ U. ran ( (,) o. g ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) e. M )
20 eleq1a 
 |-  ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) e. M -> ( z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) -> z e. M ) )
21 19 20 syl 
 |-  ( ( ( ( ph /\ z e. RR* ) /\ g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ A C_ U. ran ( (,) o. g ) ) -> ( z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) -> z e. M ) )
22 21 expimpd 
 |-  ( ( ( ph /\ z e. RR* ) /\ g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( ( A C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) -> z e. M ) )
23 22 rexlimdva 
 |-  ( ( ph /\ z e. RR* ) -> ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) -> z e. M ) )
24 23 ralrimiva 
 |-  ( ph -> A. z e. RR* ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) -> z e. M ) )
25 rabss 
 |-  ( { z e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } C_ M <-> A. z e. RR* ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) -> z e. M ) )
26 24 25 sylibr 
 |-  ( ph -> { z e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ z = sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) ) } C_ M )