Metamath Proof Explorer


Theorem ptrecube

Description: Any point in an open set of N-space is surrounded by an open cube within that set. (Contributed by Brendan Leahy, 21-Aug-2020) (Proof shortened by AV, 28-Sep-2020)

Ref Expression
Hypotheses ptrecube.r R = 𝑡 1 N × topGen ran .
ptrecube.d D = abs 2
Assertion ptrecube S R P S d + n = 1 N P n ball D d S

Proof

Step Hyp Ref Expression
1 ptrecube.r R = 𝑡 1 N × topGen ran .
2 ptrecube.d D = abs 2
3 fzfi 1 N Fin
4 retop topGen ran . Top
5 fnconstg topGen ran . Top 1 N × topGen ran . Fn 1 N
6 4 5 ax-mp 1 N × topGen ran . Fn 1 N
7 eqid x | h h Fn 1 N n 1 N h n 1 N × topGen ran . n w Fin n 1 N w h n = 1 N × topGen ran . n x = n = 1 N h n = x | h h Fn 1 N n 1 N h n 1 N × topGen ran . n w Fin n 1 N w h n = 1 N × topGen ran . n x = n = 1 N h n
8 7 ptval 1 N Fin 1 N × topGen ran . Fn 1 N 𝑡 1 N × topGen ran . = topGen x | h h Fn 1 N n 1 N h n 1 N × topGen ran . n w Fin n 1 N w h n = 1 N × topGen ran . n x = n = 1 N h n
9 3 6 8 mp2an 𝑡 1 N × topGen ran . = topGen x | h h Fn 1 N n 1 N h n 1 N × topGen ran . n w Fin n 1 N w h n = 1 N × topGen ran . n x = n = 1 N h n
10 1 9 eqtri R = topGen x | h h Fn 1 N n 1 N h n 1 N × topGen ran . n w Fin n 1 N w h n = 1 N × topGen ran . n x = n = 1 N h n
11 10 eleq2i S R S topGen x | h h Fn 1 N n 1 N h n 1 N × topGen ran . n w Fin n 1 N w h n = 1 N × topGen ran . n x = n = 1 N h n
12 tg2 S topGen x | h h Fn 1 N n 1 N h n 1 N × topGen ran . n w Fin n 1 N w h n = 1 N × topGen ran . n x = n = 1 N h n P S z x | h h Fn 1 N n 1 N h n 1 N × topGen ran . n w Fin n 1 N w h n = 1 N × topGen ran . n x = n = 1 N h n P z z S
13 7 elpt z x | h h Fn 1 N n 1 N h n 1 N × topGen ran . n w Fin n 1 N w h n = 1 N × topGen ran . n x = n = 1 N h n g g Fn 1 N n 1 N g n 1 N × topGen ran . n z Fin n 1 N z g n = 1 N × topGen ran . n z = n = 1 N g n
14 fvex topGen ran . V
15 14 fvconst2 n 1 N 1 N × topGen ran . n = topGen ran .
16 15 eleq2d n 1 N g n 1 N × topGen ran . n g n topGen ran .
17 16 ralbiia n 1 N g n 1 N × topGen ran . n n 1 N g n topGen ran .
18 elixp2 P n = 1 N g n P V P Fn 1 N n 1 N P n g n
19 18 simp3bi P n = 1 N g n n 1 N P n g n
20 r19.26 n 1 N g n topGen ran . P n g n n 1 N g n topGen ran . n 1 N P n g n
21 uniretop = topGen ran .
22 21 eltopss topGen ran . Top g n topGen ran . g n
23 4 22 mpan g n topGen ran . g n
24 23 sselda g n topGen ran . P n g n P n
25 2 rexmet D ∞Met
26 eqid MetOpen D = MetOpen D
27 2 26 tgioo topGen ran . = MetOpen D
28 27 mopni2 D ∞Met g n topGen ran . P n g n y + P n ball D y g n
29 25 28 mp3an1 g n topGen ran . P n g n y + P n ball D y g n
30 r19.42v y + P n P n ball D y g n P n y + P n ball D y g n
31 24 29 30 sylanbrc g n topGen ran . P n g n y + P n P n ball D y g n
32 31 ralimi n 1 N g n topGen ran . P n g n n 1 N y + P n P n ball D y g n
33 oveq2 y = h n P n ball D y = P n ball D h n
34 33 sseq1d y = h n P n ball D y g n P n ball D h n g n
35 34 anbi2d y = h n P n P n ball D y g n P n P n ball D h n g n
36 35 ac6sfi 1 N Fin n 1 N y + P n P n ball D y g n h h : 1 N + n 1 N P n P n ball D h n g n
37 3 32 36 sylancr n 1 N g n topGen ran . P n g n h h : 1 N + n 1 N P n P n ball D h n g n
38 1rp 1 +
39 38 a1i h : 1 N + 1 N = 1 +
40 frn h : 1 N + ran h +
41 40 adantr h : 1 N + ¬ 1 N = ran h +
42 ffn h : 1 N + h Fn 1 N
43 fnfi h Fn 1 N 1 N Fin h Fin
44 42 3 43 sylancl h : 1 N + h Fin
45 rnfi h Fin ran h Fin
46 44 45 syl h : 1 N + ran h Fin
47 46 adantr h : 1 N + ¬ 1 N = ran h Fin
48 dm0rn0 dom h = ran h =
49 fdm h : 1 N + dom h = 1 N
50 49 eqeq1d h : 1 N + dom h = 1 N =
51 48 50 bitr3id h : 1 N + ran h = 1 N =
52 51 necon3abid h : 1 N + ran h ¬ 1 N =
53 52 biimpar h : 1 N + ¬ 1 N = ran h
54 rpssre +
55 40 54 sstrdi h : 1 N + ran h
56 55 adantr h : 1 N + ¬ 1 N = ran h
57 ltso < Or
58 fiinfcl < Or ran h Fin ran h ran h sup ran h < ran h
59 57 58 mpan ran h Fin ran h ran h sup ran h < ran h
60 47 53 56 59 syl3anc h : 1 N + ¬ 1 N = sup ran h < ran h
61 41 60 sseldd h : 1 N + ¬ 1 N = sup ran h < +
62 39 61 ifclda h : 1 N + if 1 N = 1 sup ran h < +
63 62 adantr h : 1 N + n 1 N P n P n ball D h n g n if 1 N = 1 sup ran h < +
64 62 adantr h : 1 N + n 1 N if 1 N = 1 sup ran h < +
65 64 rpxrd h : 1 N + n 1 N if 1 N = 1 sup ran h < *
66 ffvelrn h : 1 N + n 1 N h n +
67 66 rpxrd h : 1 N + n 1 N h n *
68 ne0i n 1 N 1 N
69 ifnefalse 1 N if 1 N = 1 sup ran h < = sup ran h <
70 68 69 syl n 1 N if 1 N = 1 sup ran h < = sup ran h <
71 70 adantl h : 1 N + n 1 N if 1 N = 1 sup ran h < = sup ran h <
72 55 adantr h : 1 N + n 1 N ran h
73 0re 0
74 rpge0 y + 0 y
75 74 rgen y + 0 y
76 ssralv ran h + y + 0 y y ran h 0 y
77 40 75 76 mpisyl h : 1 N + y ran h 0 y
78 breq1 x = 0 x y 0 y
79 78 ralbidv x = 0 y ran h x y y ran h 0 y
80 79 rspcev 0 y ran h 0 y x y ran h x y
81 73 77 80 sylancr h : 1 N + x y ran h x y
82 81 adantr h : 1 N + n 1 N x y ran h x y
83 fnfvelrn h Fn 1 N n 1 N h n ran h
84 42 83 sylan h : 1 N + n 1 N h n ran h
85 infrelb ran h x y ran h x y h n ran h sup ran h < h n
86 72 82 84 85 syl3anc h : 1 N + n 1 N sup ran h < h n
87 71 86 eqbrtrd h : 1 N + n 1 N if 1 N = 1 sup ran h < h n
88 65 67 87 jca31 h : 1 N + n 1 N if 1 N = 1 sup ran h < * h n * if 1 N = 1 sup ran h < h n
89 ssbl D ∞Met P n if 1 N = 1 sup ran h < * h n * if 1 N = 1 sup ran h < h n P n ball D if 1 N = 1 sup ran h < P n ball D h n
90 89 3expb D ∞Met P n if 1 N = 1 sup ran h < * h n * if 1 N = 1 sup ran h < h n P n ball D if 1 N = 1 sup ran h < P n ball D h n
91 25 90 mpanl1 P n if 1 N = 1 sup ran h < * h n * if 1 N = 1 sup ran h < h n P n ball D if 1 N = 1 sup ran h < P n ball D h n
92 91 ancoms if 1 N = 1 sup ran h < * h n * if 1 N = 1 sup ran h < h n P n P n ball D if 1 N = 1 sup ran h < P n ball D h n
93 88 92 sylan h : 1 N + n 1 N P n P n ball D if 1 N = 1 sup ran h < P n ball D h n
94 sstr2 P n ball D if 1 N = 1 sup ran h < P n ball D h n P n ball D h n g n P n ball D if 1 N = 1 sup ran h < g n
95 93 94 syl h : 1 N + n 1 N P n P n ball D h n g n P n ball D if 1 N = 1 sup ran h < g n
96 95 expimpd h : 1 N + n 1 N P n P n ball D h n g n P n ball D if 1 N = 1 sup ran h < g n
97 96 ralimdva h : 1 N + n 1 N P n P n ball D h n g n n 1 N P n ball D if 1 N = 1 sup ran h < g n
98 97 imp h : 1 N + n 1 N P n P n ball D h n g n n 1 N P n ball D if 1 N = 1 sup ran h < g n
99 2 fveq2i ball D = ball abs 2
100 99 oveqi P n ball D if 1 N = 1 sup ran h < = P n ball abs 2 if 1 N = 1 sup ran h <
101 100 sseq1i P n ball D if 1 N = 1 sup ran h < g n P n ball abs 2 if 1 N = 1 sup ran h < g n
102 101 ralbii n 1 N P n ball D if 1 N = 1 sup ran h < g n n 1 N P n ball abs 2 if 1 N = 1 sup ran h < g n
103 nfv d n 1 N P n ball abs 2 if 1 N = 1 sup ran h < g n
104 102 103 nfxfr d n 1 N P n ball D if 1 N = 1 sup ran h < g n
105 oveq2 d = if 1 N = 1 sup ran h < P n ball D d = P n ball D if 1 N = 1 sup ran h <
106 105 sseq1d d = if 1 N = 1 sup ran h < P n ball D d g n P n ball D if 1 N = 1 sup ran h < g n
107 106 ralbidv d = if 1 N = 1 sup ran h < n 1 N P n ball D d g n n 1 N P n ball D if 1 N = 1 sup ran h < g n
108 104 107 rspce if 1 N = 1 sup ran h < + n 1 N P n ball D if 1 N = 1 sup ran h < g n d + n 1 N P n ball D d g n
109 63 98 108 syl2anc h : 1 N + n 1 N P n P n ball D h n g n d + n 1 N P n ball D d g n
110 109 exlimiv h h : 1 N + n 1 N P n P n ball D h n g n d + n 1 N P n ball D d g n
111 37 110 syl n 1 N g n topGen ran . P n g n d + n 1 N P n ball D d g n
112 20 111 sylbir n 1 N g n topGen ran . n 1 N P n g n d + n 1 N P n ball D d g n
113 19 112 sylan2 n 1 N g n topGen ran . P n = 1 N g n d + n 1 N P n ball D d g n
114 17 113 sylanb n 1 N g n 1 N × topGen ran . n P n = 1 N g n d + n 1 N P n ball D d g n
115 sstr2 n = 1 N P n ball D d n = 1 N g n n = 1 N g n S n = 1 N P n ball D d S
116 ss2ixp n 1 N P n ball D d g n n = 1 N P n ball D d n = 1 N g n
117 115 116 syl11 n = 1 N g n S n 1 N P n ball D d g n n = 1 N P n ball D d S
118 117 reximdv n = 1 N g n S d + n 1 N P n ball D d g n d + n = 1 N P n ball D d S
119 114 118 syl5com n 1 N g n 1 N × topGen ran . n P n = 1 N g n n = 1 N g n S d + n = 1 N P n ball D d S
120 119 expimpd n 1 N g n 1 N × topGen ran . n P n = 1 N g n n = 1 N g n S d + n = 1 N P n ball D d S
121 eleq2 z = n = 1 N g n P z P n = 1 N g n
122 sseq1 z = n = 1 N g n z S n = 1 N g n S
123 121 122 anbi12d z = n = 1 N g n P z z S P n = 1 N g n n = 1 N g n S
124 123 imbi1d z = n = 1 N g n P z z S d + n = 1 N P n ball D d S P n = 1 N g n n = 1 N g n S d + n = 1 N P n ball D d S
125 120 124 syl5ibrcom n 1 N g n 1 N × topGen ran . n z = n = 1 N g n P z z S d + n = 1 N P n ball D d S
126 125 3ad2ant2 g Fn 1 N n 1 N g n 1 N × topGen ran . n z Fin n 1 N z g n = 1 N × topGen ran . n z = n = 1 N g n P z z S d + n = 1 N P n ball D d S
127 126 imp g Fn 1 N n 1 N g n 1 N × topGen ran . n z Fin n 1 N z g n = 1 N × topGen ran . n z = n = 1 N g n P z z S d + n = 1 N P n ball D d S
128 127 exlimiv g g Fn 1 N n 1 N g n 1 N × topGen ran . n z Fin n 1 N z g n = 1 N × topGen ran . n z = n = 1 N g n P z z S d + n = 1 N P n ball D d S
129 13 128 sylbi z x | h h Fn 1 N n 1 N h n 1 N × topGen ran . n w Fin n 1 N w h n = 1 N × topGen ran . n x = n = 1 N h n P z z S d + n = 1 N P n ball D d S
130 129 rexlimiv z x | h h Fn 1 N n 1 N h n 1 N × topGen ran . n w Fin n 1 N w h n = 1 N × topGen ran . n x = n = 1 N h n P z z S d + n = 1 N P n ball D d S
131 12 130 syl S topGen x | h h Fn 1 N n 1 N h n 1 N × topGen ran . n w Fin n 1 N w h n = 1 N × topGen ran . n x = n = 1 N h n P S d + n = 1 N P n ball D d S
132 11 131 sylanb S R P S d + n = 1 N P n ball D d S