Metamath Proof Explorer

Theorem liminfresxr

Description: The inferior limit of a function only depends on the preimage of the extended real part. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminfresxr.1 
|- ( ph -> F e. V )
liminfresxr.2 
|- ( ph -> Fun F )
liminfresxr.3 
|- A = ( `' F " RR* )
Assertion liminfresxr 
|- ( ph -> ( liminf ` ( F |` A ) ) = ( liminf ` F ) )

Proof

Step Hyp Ref Expression
1 liminfresxr.1 
 |-  ( ph -> F e. V )
2 liminfresxr.2 
 |-  ( ph -> Fun F )
3 liminfresxr.3 
 |-  A = ( `' F " RR* )
4 resimass 
 |-  ( ( F |` A ) " ( k [,) +oo ) ) C_ ( F " ( k [,) +oo ) )
5 4 a1i 
 |-  ( ph -> ( ( F |` A ) " ( k [,) +oo ) ) C_ ( F " ( k [,) +oo ) ) )
6 5 ssrind 
 |-  ( ph -> ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) C_ ( ( F " ( k [,) +oo ) ) i^i RR* ) )
7 2 funfnd 
 |-  ( ph -> F Fn dom F )
8 elinel1 
 |-  ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) -> y e. ( F " ( k [,) +oo ) ) )
9 fvelima2 
 |-  ( ( F Fn dom F /\ y e. ( F " ( k [,) +oo ) ) ) -> E. x e. ( dom F i^i ( k [,) +oo ) ) ( F ` x ) = y )
10 7 8 9 syl2an 
 |-  ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> E. x e. ( dom F i^i ( k [,) +oo ) ) ( F ` x ) = y )
11 elinel1 
 |-  ( x e. ( dom F i^i ( k [,) +oo ) ) -> x e. dom F )
12 11 3ad2ant2 
 |-  ( ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> x e. dom F )
13 simpr 
 |-  ( ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ ( F ` x ) = y ) -> ( F ` x ) = y )
14 elinel2 
 |-  ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) -> y e. RR* )
15 14 adantr 
 |-  ( ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ ( F ` x ) = y ) -> y e. RR* )
16 13 15 eqeltrd 
 |-  ( ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ ( F ` x ) = y ) -> ( F ` x ) e. RR* )
17 16 3adant2 
 |-  ( ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> ( F ` x ) e. RR* )
18 12 17 jca 
 |-  ( ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> ( x e. dom F /\ ( F ` x ) e. RR* ) )
19 18 3adant1l 
 |-  ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> ( x e. dom F /\ ( F ` x ) e. RR* ) )
20 simp1l 
 |-  ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> ph )
21 elpreima 
 |-  ( F Fn dom F -> ( x e. ( `' F " RR* ) <-> ( x e. dom F /\ ( F ` x ) e. RR* ) ) )
22 7 21 syl 
 |-  ( ph -> ( x e. ( `' F " RR* ) <-> ( x e. dom F /\ ( F ` x ) e. RR* ) ) )
23 20 22 syl 
 |-  ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> ( x e. ( `' F " RR* ) <-> ( x e. dom F /\ ( F ` x ) e. RR* ) ) )
24 19 23 mpbird 
 |-  ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> x e. ( `' F " RR* ) )
25 24 3 eleqtrrdi 
 |-  ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> x e. A )
26 25 3expa 
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> x e. A )
27 26 fvresd 
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> ( ( F |` A ) ` x ) = ( F ` x ) )
28 simpr 
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> ( F ` x ) = y )
29 27 28 eqtr2d 
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> y = ( ( F |` A ) ` x ) )
30 simplll 
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> ph )
31 2 funresd 
 |-  ( ph -> Fun ( F |` A ) )
32 30 31 syl 
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> Fun ( F |` A ) )
33 11 ad2antlr 
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> x e. dom F )
34 26 33 elind 
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> x e. ( A i^i dom F ) )
35 dmres 
 |-  dom ( F |` A ) = ( A i^i dom F )
36 34 35 eleqtrrdi 
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> x e. dom ( F |` A ) )
37 32 36 jca 
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> ( Fun ( F |` A ) /\ x e. dom ( F |` A ) ) )
38 elinel2 
 |-  ( x e. ( dom F i^i ( k [,) +oo ) ) -> x e. ( k [,) +oo ) )
39 38 ad2antlr 
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> x e. ( k [,) +oo ) )
40 funfvima 
 |-  ( ( Fun ( F |` A ) /\ x e. dom ( F |` A ) ) -> ( x e. ( k [,) +oo ) -> ( ( F |` A ) ` x ) e. ( ( F |` A ) " ( k [,) +oo ) ) ) )
41 37 39 40 sylc 
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> ( ( F |` A ) ` x ) e. ( ( F |` A ) " ( k [,) +oo ) ) )
42 29 41 eqeltrd 
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> y e. ( ( F |` A ) " ( k [,) +oo ) ) )
43 42 rexlimdva2 
 |-  ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> ( E. x e. ( dom F i^i ( k [,) +oo ) ) ( F ` x ) = y -> y e. ( ( F |` A ) " ( k [,) +oo ) ) ) )
44 10 43 mpd 
 |-  ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> y e. ( ( F |` A ) " ( k [,) +oo ) ) )
45 44 ralrimiva 
 |-  ( ph -> A. y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) y e. ( ( F |` A ) " ( k [,) +oo ) ) )
46 dfss3 
 |-  ( ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ ( ( F |` A ) " ( k [,) +oo ) ) <-> A. y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) y e. ( ( F |` A ) " ( k [,) +oo ) ) )
47 45 46 sylibr 
 |-  ( ph -> ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ ( ( F |` A ) " ( k [,) +oo ) ) )
48 inss2 
 |-  ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR*
49 48 a1i 
 |-  ( ph -> ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR* )
50 47 49 ssind 
 |-  ( ph -> ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) )
51 6 50 eqssd 
 |-  ( ph -> ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) = ( ( F " ( k [,) +oo ) ) i^i RR* ) )
52 51 infeq1d 
 |-  ( ph -> inf ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
53 52 mpteq2dv 
 |-  ( ph -> ( k e. RR |-> inf ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
54 53 rneqd 
 |-  ( ph -> ran ( k e. RR |-> inf ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ran ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
55 54 supeq1d 
 |-  ( ph -> sup ( ran ( k e. RR |-> inf ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) = sup ( ran ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
56 1 resexd 
 |-  ( ph -> ( F |` A ) e. _V )
57 eqid 
 |-  ( k e. RR |-> inf ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> inf ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
58 57 liminfval 
 |-  ( ( F |` A ) e. _V -> ( liminf ` ( F |` A ) ) = sup ( ran ( k e. RR |-> inf ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
59 56 58 syl 
 |-  ( ph -> ( liminf ` ( F |` A ) ) = sup ( ran ( k e. RR |-> inf ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
60 eqid 
 |-  ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
61 60 liminfval 
 |-  ( F e. V -> ( liminf ` F ) = sup ( ran ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
62 1 61 syl 
 |-  ( ph -> ( liminf ` F ) = sup ( ran ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
63 55 59 62 3eqtr4d 
 |-  ( ph -> ( liminf ` ( F |` A ) ) = ( liminf ` F ) )