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 𝑡 Y
lmss.2 Z = M
lmss.3 φ Y V
lmss.4 φ J Top
lmss.5 φ P Y
lmss.6 φ M
lmss.7 φ F : Z Y
Assertion lmss φ F t J P F t K P

Proof

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