# 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 )`
` |-  ( ( 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 ) )`
` |-  ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) -> J e. Top )`
` |-  ( ( 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 syl6bbr
` |-  ( ( 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 )`
` |-  ( ( 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 syl6bbr
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( ph /\ ( P e. U. J /\ ran F C_ U. J ) ) /\ u e. J ) -> J e. Top )`
` |-  ( ( ( 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 ) )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( 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 ) )`