Metamath Proof Explorer


Theorem lmss

Description: Limit on a subspace. (Contributed by NM, 30-Jan-2008) (Revised by Mario Carneiro, 30-Dec-2013)

Ref Expression
Hypotheses lmss.1
|- K = ( J |`t Y )
lmss.2
|- Z = ( ZZ>= ` M )
lmss.3
|- ( ph -> Y e. V )
lmss.4
|- ( ph -> J e. Top )
lmss.5
|- ( ph -> P e. Y )
lmss.6
|- ( ph -> M e. ZZ )
lmss.7
|- ( ph -> F : Z --> Y )
Assertion lmss
|- ( ph -> ( F ( ~~>t ` J ) P <-> F ( ~~>t ` K ) P ) )

Proof

Step Hyp Ref Expression
1 lmss.1
 |-  K = ( J |`t Y )
2 lmss.2
 |-  Z = ( ZZ>= ` M )
3 lmss.3
 |-  ( ph -> Y e. V )
4 lmss.4
 |-  ( ph -> J e. Top )
5 lmss.5
 |-  ( ph -> P e. Y )
6 lmss.6
 |-  ( ph -> M e. ZZ )
7 lmss.7
 |-  ( ph -> F : Z --> Y )
8 toptopon2
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
9 4 8 sylib
 |-  ( ph -> J e. ( TopOn ` U. J ) )
10 lmcl
 |-  ( ( J e. ( TopOn ` U. J ) /\ F ( ~~>t ` J ) P ) -> P e. U. J )
11 9 10 sylan
 |-  ( ( ph /\ F ( ~~>t ` J ) P ) -> P e. U. J )
12 lmfss
 |-  ( ( J e. ( TopOn ` U. J ) /\ F ( ~~>t ` J ) P ) -> F C_ ( CC X. U. J ) )
13 9 12 sylan
 |-  ( ( ph /\ F ( ~~>t ` J ) P ) -> F C_ ( CC X. U. J ) )
14 rnss
 |-  ( F C_ ( CC X. U. J ) -> ran F C_ ran ( CC X. U. J ) )
15 13 14 syl
 |-  ( ( ph /\ F ( ~~>t ` J ) P ) -> ran F C_ ran ( CC X. U. J ) )
16 rnxpss
 |-  ran ( CC X. U. J ) C_ U. J
17 15 16 sstrdi
 |-  ( ( ph /\ F ( ~~>t ` J ) P ) -> ran F C_ U. J )
18 11 17 jca
 |-  ( ( ph /\ F ( ~~>t ` J ) P ) -> ( P e. U. J /\ ran F C_ U. J ) )
19 18 ex
 |-  ( ph -> ( F ( ~~>t ` J ) P -> ( P e. U. J /\ ran F C_ U. J ) ) )
20 resttopon2
 |-  ( ( J e. ( TopOn ` U. J ) /\ Y e. V ) -> ( J |`t Y ) e. ( TopOn ` ( Y i^i U. J ) ) )
21 9 3 20 syl2anc
 |-  ( ph -> ( J |`t Y ) e. ( TopOn ` ( Y i^i U. J ) ) )
22 1 21 eqeltrid
 |-  ( ph -> K e. ( TopOn ` ( Y i^i U. J ) ) )
23 lmcl
 |-  ( ( K e. ( TopOn ` ( Y i^i U. J ) ) /\ F ( ~~>t ` K ) P ) -> P e. ( Y i^i U. J ) )
24 22 23 sylan
 |-  ( ( ph /\ F ( ~~>t ` K ) P ) -> P e. ( Y i^i U. J ) )
25 24 elin2d
 |-  ( ( ph /\ F ( ~~>t ` K ) P ) -> P e. U. J )
26 lmfss
 |-  ( ( K e. ( TopOn ` ( Y i^i U. J ) ) /\ F ( ~~>t ` K ) P ) -> F C_ ( CC X. ( Y i^i U. J ) ) )
27 22 26 sylan
 |-  ( ( ph /\ F ( ~~>t ` K ) P ) -> F C_ ( CC X. ( Y i^i U. J ) ) )
28 rnss
 |-  ( F C_ ( CC X. ( Y i^i U. J ) ) -> ran F C_ ran ( CC X. ( Y i^i U. J ) ) )
29 27 28 syl
 |-  ( ( ph /\ F ( ~~>t ` K ) P ) -> ran F C_ ran ( CC X. ( Y i^i U. J ) ) )
30 rnxpss
 |-  ran ( CC X. ( Y i^i U. J ) ) C_ ( Y i^i U. J )
31 29 30 sstrdi
 |-  ( ( ph /\ F ( ~~>t ` K ) P ) -> ran F C_ ( Y i^i U. J ) )
32 inss2
 |-  ( Y i^i U. J ) C_ U. J
33 31 32 sstrdi
 |-  ( ( ph /\ F ( ~~>t ` K ) P ) -> ran F C_ U. J )
34 25 33 jca
 |-  ( ( ph /\ F ( ~~>t ` K ) P ) -> ( P e. U. J /\ ran F C_ U. J ) )
35 34 ex
 |-  ( ph -> ( F ( ~~>t ` K ) P -> ( P e. U. J /\ ran F C_ U. J ) ) )
36 simprl
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> P e. U. J )
37 5 adantr
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> P e. Y )
38 37 36 elind
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> P e. ( Y i^i U. J ) )
39 36 38 2thd
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( P e. U. J <-> P e. ( Y i^i U. J ) ) )
40 1 eleq2i
 |-  ( v e. K <-> v e. ( J |`t Y ) )
41 4 adantr
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> J e. Top )
42 3 adantr
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> Y e. V )
43 elrest
 |-  ( ( J e. Top /\ Y e. V ) -> ( v e. ( J |`t Y ) <-> E. u e. J v = ( u i^i Y ) ) )
44 41 42 43 syl2anc
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( v e. ( J |`t Y ) <-> E. u e. J v = ( u i^i Y ) ) )
45 44 biimpa
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ v e. ( J |`t Y ) ) -> E. u e. J v = ( u i^i Y ) )
46 40 45 sylan2b
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ v e. K ) -> E. u e. J v = ( u i^i Y ) )
47 r19.29r
 |-  ( ( E. u e. J v = ( u i^i Y ) /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) -> E. u e. J ( v = ( u i^i Y ) /\ ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) )
48 37 biantrud
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( P e. u <-> ( P e. u /\ P e. Y ) ) )
49 elin
 |-  ( P e. ( u i^i Y ) <-> ( P e. u /\ P e. Y ) )
50 48 49 bitr4di
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( P e. u <-> P e. ( u i^i Y ) ) )
51 2 uztrn2
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
52 7 adantr
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> F : Z --> Y )
53 52 ffvelrnda
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ k e. Z ) -> ( F ` k ) e. Y )
54 53 biantrud
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ k e. Z ) -> ( ( F ` k ) e. u <-> ( ( F ` k ) e. u /\ ( F ` k ) e. Y ) ) )
55 elin
 |-  ( ( F ` k ) e. ( u i^i Y ) <-> ( ( F ` k ) e. u /\ ( F ` k ) e. Y ) )
56 54 55 bitr4di
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ k e. Z ) -> ( ( F ` k ) e. u <-> ( F ` k ) e. ( u i^i Y ) ) )
57 51 56 sylan2
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( F ` k ) e. u <-> ( F ` k ) e. ( u i^i Y ) ) )
58 57 anassrs
 |-  ( ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) e. u <-> ( F ` k ) e. ( u i^i Y ) ) )
59 58 ralbidva
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( F ` k ) e. u <-> A. k e. ( ZZ>= ` j ) ( F ` k ) e. ( u i^i Y ) ) )
60 59 rexbidva
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. ( u i^i Y ) ) )
61 50 60 imbi12d
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) <-> ( P e. ( u i^i Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. ( u i^i Y ) ) ) )
62 61 adantr
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ u e. J ) -> ( ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) <-> ( P e. ( u i^i Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. ( u i^i Y ) ) ) )
63 62 biimpd
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ u e. J ) -> ( ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) -> ( P e. ( u i^i Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. ( u i^i Y ) ) ) )
64 eleq2
 |-  ( v = ( u i^i Y ) -> ( P e. v <-> P e. ( u i^i Y ) ) )
65 eleq2
 |-  ( v = ( u i^i Y ) -> ( ( F ` k ) e. v <-> ( F ` k ) e. ( u i^i Y ) ) )
66 65 rexralbidv
 |-  ( v = ( u i^i Y ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. ( u i^i Y ) ) )
67 64 66 imbi12d
 |-  ( v = ( u i^i Y ) -> ( ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) <-> ( P e. ( u i^i Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. ( u i^i Y ) ) ) )
68 67 imbi2d
 |-  ( v = ( u i^i Y ) -> ( ( ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) -> ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) ) <-> ( ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) -> ( P e. ( u i^i Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. ( u i^i Y ) ) ) ) )
69 63 68 syl5ibrcom
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ u e. J ) -> ( v = ( u i^i Y ) -> ( ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) -> ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) ) ) )
70 69 impd
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ u e. J ) -> ( ( v = ( u i^i Y ) /\ ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) -> ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) ) )
71 70 rexlimdva
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( E. u e. J ( v = ( u i^i Y ) /\ ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) -> ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) ) )
72 47 71 syl5
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( ( E. u e. J v = ( u i^i Y ) /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) -> ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) ) )
73 72 expdimp
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ E. u e. J v = ( u i^i Y ) ) -> ( A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) -> ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) ) )
74 46 73 syldan
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ v e. K ) -> ( A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) -> ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) ) )
75 74 ralrimdva
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) -> A. v e. K ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) ) )
76 41 adantr
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ u e. J ) -> J e. Top )
77 42 adantr
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ u e. J ) -> Y e. V )
78 simpr
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ u e. J ) -> u e. J )
79 elrestr
 |-  ( ( J e. Top /\ Y e. V /\ u e. J ) -> ( u i^i Y ) e. ( J |`t Y ) )
80 76 77 78 79 syl3anc
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ u e. J ) -> ( u i^i Y ) e. ( J |`t Y ) )
81 80 1 eleqtrrdi
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ u e. J ) -> ( u i^i Y ) e. K )
82 67 rspcv
 |-  ( ( u i^i Y ) e. K -> ( A. v e. K ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) -> ( P e. ( u i^i Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. ( u i^i Y ) ) ) )
83 81 82 syl
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ u e. J ) -> ( A. v e. K ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) -> ( P e. ( u i^i Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. ( u i^i Y ) ) ) )
84 83 62 sylibrd
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ u e. J ) -> ( A. v e. K ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) -> ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) )
85 84 ralrimdva
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( A. v e. K ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) -> A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) )
86 75 85 impbid
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) <-> A. v e. K ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) ) )
87 39 86 anbi12d
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( ( P e. U. J /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) <-> ( P e. ( Y i^i U. J ) /\ A. v e. K ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) ) ) )
88 41 8 sylib
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> J e. ( TopOn ` U. J ) )
89 6 adantr
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> M e. ZZ )
90 52 ffnd
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> F Fn Z )
91 simprr
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ran F C_ U. J )
92 df-f
 |-  ( F : Z --> U. J <-> ( F Fn Z /\ ran F C_ U. J ) )
93 90 91 92 sylanbrc
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> F : Z --> U. J )
94 eqidd
 |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
95 88 2 89 93 94 lmbrf
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( F ( ~~>t ` J ) P <-> ( P e. U. J /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) ) )
96 22 adantr
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> K e. ( TopOn ` ( Y i^i U. J ) ) )
97 52 frnd
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ran F C_ Y )
98 97 91 ssind
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ran F C_ ( Y i^i U. J ) )
99 df-f
 |-  ( F : Z --> ( Y i^i U. J ) <-> ( F Fn Z /\ ran F C_ ( Y i^i U. J ) ) )
100 90 98 99 sylanbrc
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> F : Z --> ( Y i^i U. J ) )
101 96 2 89 100 94 lmbrf
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( F ( ~~>t ` K ) P <-> ( P e. ( Y i^i U. J ) /\ A. v e. K ( P e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. v ) ) ) )
102 87 95 101 3bitr4d
 |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> ( F ( ~~>t ` J ) P <-> F ( ~~>t ` K ) P ) )
103 102 ex
 |-  ( ph -> ( ( P e. U. J /\ ran F C_ U. J ) -> ( F ( ~~>t ` J ) P <-> F ( ~~>t ` K ) P ) ) )
104 19 35 103 pm5.21ndd
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> F ( ~~>t ` K ) P ) )