Metamath Proof Explorer

Theorem rlimres

Description: The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Assertion rlimres 
|- ( F ~~>r A -> ( F |` B ) ~~>r A )

Proof

Step Hyp Ref Expression
1 inss1 
 |-  ( dom F i^i B ) C_ dom F
2 ssralv 
 |-  ( ( dom F i^i B ) C_ dom F -> ( A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) -> A. z e. ( dom F i^i B ) ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) ) )
3 1 2 ax-mp 
 |-  ( A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) -> A. z e. ( dom F i^i B ) ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) )
4 3 reximi 
 |-  ( E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) -> E. y e. RR A. z e. ( dom F i^i B ) ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) )
5 4 ralimi 
 |-  ( A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) -> A. x e. RR+ E. y e. RR A. z e. ( dom F i^i B ) ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) )
6 5 anim2i 
 |-  ( ( A e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) ) -> ( A e. CC /\ A. x e. RR+ E. y e. RR A. z e. ( dom F i^i B ) ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) ) )
7 6 a1i 
 |-  ( F ~~>r A -> ( ( A e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) ) -> ( A e. CC /\ A. x e. RR+ E. y e. RR A. z e. ( dom F i^i B ) ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) ) ) )
8 rlimf 
 |-  ( F ~~>r A -> F : dom F --> CC )
9 rlimss 
 |-  ( F ~~>r A -> dom F C_ RR )
10 eqidd 
 |-  ( ( F ~~>r A /\ z e. dom F ) -> ( F ` z ) = ( F ` z ) )
11 8 9 10 rlim 
 |-  ( F ~~>r A -> ( F ~~>r A <-> ( A e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) ) ) )
12 fssres 
 |-  ( ( F : dom F --> CC /\ ( dom F i^i B ) C_ dom F ) -> ( F |` ( dom F i^i B ) ) : ( dom F i^i B ) --> CC )
13 8 1 12 sylancl 
 |-  ( F ~~>r A -> ( F |` ( dom F i^i B ) ) : ( dom F i^i B ) --> CC )
14 resres 
 |-  ( ( F |` dom F ) |` B ) = ( F |` ( dom F i^i B ) )
15 ffn 
 |-  ( F : dom F --> CC -> F Fn dom F )
16 fnresdm 
 |-  ( F Fn dom F -> ( F |` dom F ) = F )
17 8 15 16 3syl 
 |-  ( F ~~>r A -> ( F |` dom F ) = F )
18 17 reseq1d 
 |-  ( F ~~>r A -> ( ( F |` dom F ) |` B ) = ( F |` B ) )
19 14 18 eqtr3id 
 |-  ( F ~~>r A -> ( F |` ( dom F i^i B ) ) = ( F |` B ) )
20 19 feq1d 
 |-  ( F ~~>r A -> ( ( F |` ( dom F i^i B ) ) : ( dom F i^i B ) --> CC <-> ( F |` B ) : ( dom F i^i B ) --> CC ) )
21 13 20 mpbid 
 |-  ( F ~~>r A -> ( F |` B ) : ( dom F i^i B ) --> CC )
22 1 9 sstrid 
 |-  ( F ~~>r A -> ( dom F i^i B ) C_ RR )
23 elinel2 
 |-  ( z e. ( dom F i^i B ) -> z e. B )
24 23 fvresd 
 |-  ( z e. ( dom F i^i B ) -> ( ( F |` B ) ` z ) = ( F ` z ) )
25 24 adantl 
 |-  ( ( F ~~>r A /\ z e. ( dom F i^i B ) ) -> ( ( F |` B ) ` z ) = ( F ` z ) )
26 21 22 25 rlim 
 |-  ( F ~~>r A -> ( ( F |` B ) ~~>r A <-> ( A e. CC /\ A. x e. RR+ E. y e. RR A. z e. ( dom F i^i B ) ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < x ) ) ) )
27 7 11 26 3imtr4d 
 |-  ( F ~~>r A -> ( F ~~>r A -> ( F |` B ) ~~>r A ) )
28 27 pm2.43i 
 |-  ( F ~~>r A -> ( F |` B ) ~~>r A )