Metamath Proof Explorer


Theorem poimir

Description: Poincare-Miranda theorem. Theorem on Kulpa p. 547. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 φ N
poimir.i I = 0 1 1 N
poimir.r R = 𝑡 1 N × topGen ran .
poimir.1 φ F R 𝑡 I Cn R
poimir.2 φ n 1 N z I z n = 0 F z n 0
poimir.3 φ n 1 N z I z n = 1 0 F z n
Assertion poimir φ c I F c = 1 N × 0

Proof

Step Hyp Ref Expression
1 poimir.0 φ N
2 poimir.i I = 0 1 1 N
3 poimir.r R = 𝑡 1 N × topGen ran .
4 poimir.1 φ F R 𝑡 I Cn R
5 poimir.2 φ n 1 N z I z n = 0 F z n 0
6 poimir.3 φ n 1 N z I z n = 1 0 F z n
7 1 2 3 4 5 6 poimirlem32 φ c I n 1 N v R 𝑡 I c v r -1 z v 0 r F z n
8 ovex 1 N V
9 retopon topGen ran . TopOn
10 3 pttoponconst 1 N V topGen ran . TopOn R TopOn 1 N
11 8 9 10 mp2an R TopOn 1 N
12 11 topontopi R Top
13 reex V
14 unitssre 0 1
15 mapss V 0 1 0 1 1 N 1 N
16 13 14 15 mp2an 0 1 1 N 1 N
17 2 16 eqsstri I 1 N
18 11 toponunii 1 N = R
19 18 restuni R Top I 1 N I = R 𝑡 I
20 12 17 19 mp2an I = R 𝑡 I
21 20 18 cnf F R 𝑡 I Cn R F : I 1 N
22 4 21 syl φ F : I 1 N
23 22 ffvelrnda φ c I F c 1 N
24 elmapi F c 1 N F c : 1 N
25 23 24 syl φ c I F c : 1 N
26 25 ffvelrnda φ c I n 1 N F c n
27 recn F c n F c n
28 absrpcl F c n F c n 0 F c n +
29 28 ex F c n F c n 0 F c n +
30 27 29 syl F c n F c n 0 F c n +
31 ltsubrp F c n F c n + F c n F c n < F c n
32 ltaddrp F c n F c n + F c n < F c n + F c n
33 31 32 jca F c n F c n + F c n F c n < F c n F c n < F c n + F c n
34 33 ex F c n F c n + F c n F c n < F c n F c n < F c n + F c n
35 30 34 syld F c n F c n 0 F c n F c n < F c n F c n < F c n + F c n
36 27 abscld F c n F c n
37 resubcl F c n F c n F c n F c n
38 36 37 mpdan F c n F c n F c n
39 38 rexrd F c n F c n F c n *
40 readdcl F c n F c n F c n + F c n
41 36 40 mpdan F c n F c n + F c n
42 41 rexrd F c n F c n + F c n *
43 rexr F c n F c n *
44 elioo5 F c n F c n * F c n + F c n * F c n * F c n F c n F c n F c n + F c n F c n F c n < F c n F c n < F c n + F c n
45 39 42 43 44 syl3anc F c n F c n F c n F c n F c n + F c n F c n F c n < F c n F c n < F c n + F c n
46 35 45 sylibrd F c n F c n 0 F c n F c n F c n F c n + F c n
47 26 46 syl φ c I n 1 N F c n 0 F c n F c n F c n F c n + F c n
48 fveq2 x = c F x = F c
49 48 fveq1d x = c F x n = F c n
50 eqid x I F x n = x I F x n
51 fvex F c n V
52 49 50 51 fvmpt c I x I F x n c = F c n
53 52 eleq1d c I x I F x n c F c n F c n F c n + F c n F c n F c n F c n F c n + F c n
54 53 ad2antlr φ c I n 1 N x I F x n c F c n F c n F c n + F c n F c n F c n F c n F c n + F c n
55 47 54 sylibrd φ c I n 1 N F c n 0 x I F x n c F c n F c n F c n + F c n
56 iooretop F c n F c n F c n + F c n topGen ran .
57 resttopon R TopOn 1 N I 1 N R 𝑡 I TopOn I
58 11 17 57 mp2an R 𝑡 I TopOn I
59 58 a1i φ n 1 N R 𝑡 I TopOn I
60 22 feqmptd φ F = x I F x
61 60 4 eqeltrrd φ x I F x R 𝑡 I Cn R
62 61 adantr φ n 1 N x I F x R 𝑡 I Cn R
63 11 a1i φ n 1 N R TopOn 1 N
64 retop topGen ran . Top
65 64 fconst6 1 N × topGen ran . : 1 N Top
66 18 3 ptpjcn 1 N V 1 N × topGen ran . : 1 N Top n 1 N z 1 N z n R Cn 1 N × topGen ran . n
67 8 65 66 mp3an12 n 1 N z 1 N z n R Cn 1 N × topGen ran . n
68 fvex topGen ran . V
69 68 fvconst2 n 1 N 1 N × topGen ran . n = topGen ran .
70 69 oveq2d n 1 N R Cn 1 N × topGen ran . n = R Cn topGen ran .
71 67 70 eleqtrd n 1 N z 1 N z n R Cn topGen ran .
72 71 adantl φ n 1 N z 1 N z n R Cn topGen ran .
73 fveq1 z = F x z n = F x n
74 59 62 63 72 73 cnmpt11 φ n 1 N x I F x n R 𝑡 I Cn topGen ran .
75 20 cncnpi x I F x n R 𝑡 I Cn topGen ran . c I x I F x n R 𝑡 I CnP topGen ran . c
76 74 75 sylan φ n 1 N c I x I F x n R 𝑡 I CnP topGen ran . c
77 76 an32s φ c I n 1 N x I F x n R 𝑡 I CnP topGen ran . c
78 iscnp R 𝑡 I TopOn I topGen ran . TopOn c I x I F x n R 𝑡 I CnP topGen ran . c x I F x n : I z topGen ran . x I F x n c z v R 𝑡 I c v x I F x n v z
79 58 9 78 mp3an12 c I x I F x n R 𝑡 I CnP topGen ran . c x I F x n : I z topGen ran . x I F x n c z v R 𝑡 I c v x I F x n v z
80 79 ad2antlr φ c I n 1 N x I F x n R 𝑡 I CnP topGen ran . c x I F x n : I z topGen ran . x I F x n c z v R 𝑡 I c v x I F x n v z
81 77 80 mpbid φ c I n 1 N x I F x n : I z topGen ran . x I F x n c z v R 𝑡 I c v x I F x n v z
82 81 simprd φ c I n 1 N z topGen ran . x I F x n c z v R 𝑡 I c v x I F x n v z
83 eleq2 z = F c n F c n F c n + F c n x I F x n c z x I F x n c F c n F c n F c n + F c n
84 sseq2 z = F c n F c n F c n + F c n x I F x n v z x I F x n v F c n F c n F c n + F c n
85 84 anbi2d z = F c n F c n F c n + F c n c v x I F x n v z c v x I F x n v F c n F c n F c n + F c n
86 85 rexbidv z = F c n F c n F c n + F c n v R 𝑡 I c v x I F x n v z v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n
87 83 86 imbi12d z = F c n F c n F c n + F c n x I F x n c z v R 𝑡 I c v x I F x n v z x I F x n c F c n F c n F c n + F c n v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n
88 87 rspcv F c n F c n F c n + F c n topGen ran . z topGen ran . x I F x n c z v R 𝑡 I c v x I F x n v z x I F x n c F c n F c n F c n + F c n v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n
89 56 82 88 mpsyl φ c I n 1 N x I F x n c F c n F c n F c n + F c n v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n
90 55 89 syld φ c I n 1 N F c n 0 v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n
91 0re 0
92 letric F c n 0 F c n 0 0 F c n
93 26 91 92 sylancl φ c I n 1 N F c n 0 0 F c n
94 90 93 jctird φ c I n 1 N F c n 0 v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n
95 r19.41v v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n
96 anass c v x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n c v x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n
97 96 rexbii v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n
98 95 97 bitr3i v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n
99 94 98 syl6ib φ c I n 1 N F c n 0 v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n
100 58 topontopi R 𝑡 I Top
101 20 eltopss R 𝑡 I Top v R 𝑡 I v I
102 100 101 mpan v R 𝑡 I v I
103 fvex F x n V
104 103 50 dmmpti dom x I F x n = I
105 104 sseq2i v dom x I F x n v I
106 funmpt Fun x I F x n
107 funimass4 Fun x I F x n v dom x I F x n x I F x n v F c n F c n F c n + F c n z v x I F x n z F c n F c n F c n + F c n
108 106 107 mpan v dom x I F x n x I F x n v F c n F c n F c n + F c n z v x I F x n z F c n F c n F c n + F c n
109 105 108 sylbir v I x I F x n v F c n F c n F c n + F c n z v x I F x n z F c n F c n F c n + F c n
110 ssel2 v I z v z I
111 fveq2 x = z F x = F z
112 111 fveq1d x = z F x n = F z n
113 fvex F z n V
114 112 50 113 fvmpt z I x I F x n z = F z n
115 114 eleq1d z I x I F x n z F c n F c n F c n + F c n F z n F c n F c n F c n + F c n
116 eliooord F z n F c n F c n F c n + F c n F c n F c n < F z n F z n < F c n + F c n
117 115 116 syl6bi z I x I F x n z F c n F c n F c n + F c n F c n F c n < F z n F z n < F c n + F c n
118 110 117 syl v I z v x I F x n z F c n F c n F c n + F c n F c n F c n < F z n F z n < F c n + F c n
119 118 ralimdva v I z v x I F x n z F c n F c n F c n + F c n z v F c n F c n < F z n F z n < F c n + F c n
120 109 119 sylbid v I x I F x n v F c n F c n F c n + F c n z v F c n F c n < F z n F z n < F c n + F c n
121 120 adantl φ c I n 1 N v I x I F x n v F c n F c n F c n + F c n z v F c n F c n < F z n F z n < F c n + F c n
122 absnid F c n F c n 0 F c n = F c n
123 122 oveq2d F c n F c n 0 F c n + F c n = F c n + F c n
124 27 negidd F c n F c n + F c n = 0
125 124 adantr F c n F c n 0 F c n + F c n = 0
126 123 125 eqtrd F c n F c n 0 F c n + F c n = 0
127 26 126 sylan φ c I n 1 N F c n 0 F c n + F c n = 0
128 127 adantr φ c I n 1 N F c n 0 z I F c n + F c n = 0
129 128 breq2d φ c I n 1 N F c n 0 z I F z n < F c n + F c n F z n < 0
130 22 ffvelrnda φ z I F z 1 N
131 elmapi F z 1 N F z : 1 N
132 130 131 syl φ z I F z : 1 N
133 132 ffvelrnda φ z I n 1 N F z n
134 133 an32s φ n 1 N z I F z n
135 0red φ n 1 N z I 0
136 134 135 ltnled φ n 1 N z I F z n < 0 ¬ 0 F z n
137 136 adantllr φ c I n 1 N z I F z n < 0 ¬ 0 F z n
138 137 adantlr φ c I n 1 N F c n 0 z I F z n < 0 ¬ 0 F z n
139 129 138 bitrd φ c I n 1 N F c n 0 z I F z n < F c n + F c n ¬ 0 F z n
140 139 biimpd φ c I n 1 N F c n 0 z I F z n < F c n + F c n ¬ 0 F z n
141 110 140 sylan2 φ c I n 1 N F c n 0 v I z v F z n < F c n + F c n ¬ 0 F z n
142 141 anassrs φ c I n 1 N F c n 0 v I z v F z n < F c n + F c n ¬ 0 F z n
143 142 adantld φ c I n 1 N F c n 0 v I z v F c n F c n < F z n F z n < F c n + F c n ¬ 0 F z n
144 143 ralimdva φ c I n 1 N F c n 0 v I z v F c n F c n < F z n F z n < F c n + F c n z v ¬ 0 F z n
145 144 an32s φ c I n 1 N v I F c n 0 z v F c n F c n < F z n F z n < F c n + F c n z v ¬ 0 F z n
146 145 impancom φ c I n 1 N v I z v F c n F c n < F z n F z n < F c n + F c n F c n 0 z v ¬ 0 F z n
147 absid F c n 0 F c n F c n = F c n
148 147 oveq2d F c n 0 F c n F c n F c n = F c n F c n
149 27 subidd F c n F c n F c n = 0
150 149 adantr F c n 0 F c n F c n F c n = 0
151 148 150 eqtrd F c n 0 F c n F c n F c n = 0
152 26 151 sylan φ c I n 1 N 0 F c n F c n F c n = 0
153 152 adantr φ c I n 1 N 0 F c n z I F c n F c n = 0
154 153 breq1d φ c I n 1 N 0 F c n z I F c n F c n < F z n 0 < F z n
155 135 134 ltnled φ n 1 N z I 0 < F z n ¬ F z n 0
156 155 adantllr φ c I n 1 N z I 0 < F z n ¬ F z n 0
157 156 adantlr φ c I n 1 N 0 F c n z I 0 < F z n ¬ F z n 0
158 154 157 bitrd φ c I n 1 N 0 F c n z I F c n F c n < F z n ¬ F z n 0
159 158 biimpd φ c I n 1 N 0 F c n z I F c n F c n < F z n ¬ F z n 0
160 110 159 sylan2 φ c I n 1 N 0 F c n v I z v F c n F c n < F z n ¬ F z n 0
161 160 anassrs φ c I n 1 N 0 F c n v I z v F c n F c n < F z n ¬ F z n 0
162 161 adantrd φ c I n 1 N 0 F c n v I z v F c n F c n < F z n F z n < F c n + F c n ¬ F z n 0
163 162 ralimdva φ c I n 1 N 0 F c n v I z v F c n F c n < F z n F z n < F c n + F c n z v ¬ F z n 0
164 163 an32s φ c I n 1 N v I 0 F c n z v F c n F c n < F z n F z n < F c n + F c n z v ¬ F z n 0
165 164 impancom φ c I n 1 N v I z v F c n F c n < F z n F z n < F c n + F c n 0 F c n z v ¬ F z n 0
166 146 165 orim12d φ c I n 1 N v I z v F c n F c n < F z n F z n < F c n + F c n F c n 0 0 F c n z v ¬ 0 F z n z v ¬ F z n 0
167 166 expimpd φ c I n 1 N v I z v F c n F c n < F z n F z n < F c n + F c n F c n 0 0 F c n z v ¬ 0 F z n z v ¬ F z n 0
168 121 167 syland φ c I n 1 N v I x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n z v ¬ 0 F z n z v ¬ F z n 0
169 102 168 sylan2 φ c I n 1 N v R 𝑡 I x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n z v ¬ 0 F z n z v ¬ F z n 0
170 169 anim2d φ c I n 1 N v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n c v z v ¬ 0 F z n z v ¬ F z n 0
171 170 reximdva φ c I n 1 N v R 𝑡 I c v x I F x n v F c n F c n F c n + F c n F c n 0 0 F c n v R 𝑡 I c v z v ¬ 0 F z n z v ¬ F z n 0
172 99 171 syld φ c I n 1 N F c n 0 v R 𝑡 I c v z v ¬ 0 F z n z v ¬ F z n 0
173 ralnex z v ¬ 0 r F z n ¬ z v 0 r F z n
174 173 rexbii r -1 z v ¬ 0 r F z n r -1 ¬ z v 0 r F z n
175 letsr TosetRel
176 175 elexi V
177 176 cnvex -1 V
178 breq r = 0 r F z n 0 F z n
179 178 notbid r = ¬ 0 r F z n ¬ 0 F z n
180 179 ralbidv r = z v ¬ 0 r F z n z v ¬ 0 F z n
181 breq r = -1 0 r F z n 0 -1 F z n
182 c0ex 0 V
183 182 113 brcnv 0 -1 F z n F z n 0
184 181 183 bitrdi r = -1 0 r F z n F z n 0
185 184 notbid r = -1 ¬ 0 r F z n ¬ F z n 0
186 185 ralbidv r = -1 z v ¬ 0 r F z n z v ¬ F z n 0
187 176 177 180 186 rexpr r -1 z v ¬ 0 r F z n z v ¬ 0 F z n z v ¬ F z n 0
188 rexnal r -1 ¬ z v 0 r F z n ¬ r -1 z v 0 r F z n
189 174 187 188 3bitr3i z v ¬ 0 F z n z v ¬ F z n 0 ¬ r -1 z v 0 r F z n
190 189 anbi2i c v z v ¬ 0 F z n z v ¬ F z n 0 c v ¬ r -1 z v 0 r F z n
191 annim c v ¬ r -1 z v 0 r F z n ¬ c v r -1 z v 0 r F z n
192 190 191 bitri c v z v ¬ 0 F z n z v ¬ F z n 0 ¬ c v r -1 z v 0 r F z n
193 192 rexbii v R 𝑡 I c v z v ¬ 0 F z n z v ¬ F z n 0 v R 𝑡 I ¬ c v r -1 z v 0 r F z n
194 rexnal v R 𝑡 I ¬ c v r -1 z v 0 r F z n ¬ v R 𝑡 I c v r -1 z v 0 r F z n
195 193 194 bitri v R 𝑡 I c v z v ¬ 0 F z n z v ¬ F z n 0 ¬ v R 𝑡 I c v r -1 z v 0 r F z n
196 172 195 syl6ib φ c I n 1 N F c n 0 ¬ v R 𝑡 I c v r -1 z v 0 r F z n
197 196 necon4ad φ c I n 1 N v R 𝑡 I c v r -1 z v 0 r F z n F c n = 0
198 197 ralimdva φ c I n 1 N v R 𝑡 I c v r -1 z v 0 r F z n n 1 N F c n = 0
199 25 ffnd φ c I F c Fn 1 N
200 198 199 jctild φ c I n 1 N v R 𝑡 I c v r -1 z v 0 r F z n F c Fn 1 N n 1 N F c n = 0
201 fconstfv F c : 1 N 0 F c Fn 1 N n 1 N F c n = 0
202 182 fconst2 F c : 1 N 0 F c = 1 N × 0
203 201 202 bitr3i F c Fn 1 N n 1 N F c n = 0 F c = 1 N × 0
204 200 203 syl6ib φ c I n 1 N v R 𝑡 I c v r -1 z v 0 r F z n F c = 1 N × 0
205 204 reximdva φ c I n 1 N v R 𝑡 I c v r -1 z v 0 r F z n c I F c = 1 N × 0
206 7 205 mpd φ c I F c = 1 N × 0