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 )