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 ) )