Metamath Proof Explorer

Theorem cnheiborlem

Description: Lemma for cnheibor . (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses cnheibor.2 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
cnheibor.3 ${⊢}{T}={J}{↾}_{𝑡}{X}$
cnheibor.4 ${⊢}{F}=\left({x}\in ℝ,{y}\in ℝ⟼{x}+\mathrm{i}{y}\right)$
cnheibor.5 ${⊢}{Y}={F}\left[\left[-{R},{R}\right]×\left[-{R},{R}\right]\right]$
Assertion cnheiborlem ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to {T}\in \mathrm{Comp}$

Proof

Step Hyp Ref Expression
1 cnheibor.2 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 cnheibor.3 ${⊢}{T}={J}{↾}_{𝑡}{X}$
3 cnheibor.4 ${⊢}{F}=\left({x}\in ℝ,{y}\in ℝ⟼{x}+\mathrm{i}{y}\right)$
4 cnheibor.5 ${⊢}{Y}={F}\left[\left[-{R},{R}\right]×\left[-{R},{R}\right]\right]$
5 1 cnfldtop ${⊢}{J}\in \mathrm{Top}$
6 3 cnref1o ${⊢}{F}:{ℝ}^{2}\underset{1-1 onto}{⟶}ℂ$
7 f1ofn ${⊢}{F}:{ℝ}^{2}\underset{1-1 onto}{⟶}ℂ\to {F}Fn{ℝ}^{2}$
8 elpreima ${⊢}{F}Fn{ℝ}^{2}\to \left({u}\in {{F}}^{-1}\left[{X}\right]↔\left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)$
9 6 7 8 mp2b ${⊢}{u}\in {{F}}^{-1}\left[{X}\right]↔\left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)$
10 1st2nd2 ${⊢}{u}\in {ℝ}^{2}\to {u}=⟨{1}^{st}\left({u}\right),{2}^{nd}\left({u}\right)⟩$
11 10 ad2antrl ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {u}=⟨{1}^{st}\left({u}\right),{2}^{nd}\left({u}\right)⟩$
12 xp1st ${⊢}{u}\in {ℝ}^{2}\to {1}^{st}\left({u}\right)\in ℝ$
13 12 ad2antrl ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {1}^{st}\left({u}\right)\in ℝ$
14 13 recnd ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {1}^{st}\left({u}\right)\in ℂ$
15 14 abscld ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left|{1}^{st}\left({u}\right)\right|\in ℝ$
16 1 cnfldtopon ${⊢}{J}\in \mathrm{TopOn}\left(ℂ\right)$
17 16 toponunii ${⊢}ℂ=\bigcup {J}$
18 17 cldss ${⊢}{X}\in \mathrm{Clsd}\left({J}\right)\to {X}\subseteq ℂ$
19 18 adantr ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to {X}\subseteq ℂ$
20 19 adantr ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {X}\subseteq ℂ$
21 simprr ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {F}\left({u}\right)\in {X}$
22 20 21 sseldd ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {F}\left({u}\right)\in ℂ$
23 22 abscld ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left|{F}\left({u}\right)\right|\in ℝ$
24 simplrl ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {R}\in ℝ$
25 simprl ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {u}\in {ℝ}^{2}$
26 f1ocnvfv1 ${⊢}\left({F}:{ℝ}^{2}\underset{1-1 onto}{⟶}ℂ\wedge {u}\in {ℝ}^{2}\right)\to {{F}}^{-1}\left({F}\left({u}\right)\right)={u}$
27 6 25 26 sylancr ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {{F}}^{-1}\left({F}\left({u}\right)\right)={u}$
28 fveq2 ${⊢}{z}={F}\left({u}\right)\to \Re \left({z}\right)=\Re \left({F}\left({u}\right)\right)$
29 fveq2 ${⊢}{z}={F}\left({u}\right)\to \Im \left({z}\right)=\Im \left({F}\left({u}\right)\right)$
30 28 29 opeq12d ${⊢}{z}={F}\left({u}\right)\to ⟨\Re \left({z}\right),\Im \left({z}\right)⟩=⟨\Re \left({F}\left({u}\right)\right),\Im \left({F}\left({u}\right)\right)⟩$
31 3 cnrecnv ${⊢}{{F}}^{-1}=\left({z}\in ℂ⟼⟨\Re \left({z}\right),\Im \left({z}\right)⟩\right)$
32 opex ${⊢}⟨\Re \left({F}\left({u}\right)\right),\Im \left({F}\left({u}\right)\right)⟩\in \mathrm{V}$
33 30 31 32 fvmpt ${⊢}{F}\left({u}\right)\in ℂ\to {{F}}^{-1}\left({F}\left({u}\right)\right)=⟨\Re \left({F}\left({u}\right)\right),\Im \left({F}\left({u}\right)\right)⟩$
34 22 33 syl ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {{F}}^{-1}\left({F}\left({u}\right)\right)=⟨\Re \left({F}\left({u}\right)\right),\Im \left({F}\left({u}\right)\right)⟩$
35 27 34 eqtr3d ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {u}=⟨\Re \left({F}\left({u}\right)\right),\Im \left({F}\left({u}\right)\right)⟩$
36 35 fveq2d ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {1}^{st}\left({u}\right)={1}^{st}\left(⟨\Re \left({F}\left({u}\right)\right),\Im \left({F}\left({u}\right)\right)⟩\right)$
37 fvex ${⊢}\Re \left({F}\left({u}\right)\right)\in \mathrm{V}$
38 fvex ${⊢}\Im \left({F}\left({u}\right)\right)\in \mathrm{V}$
39 37 38 op1st ${⊢}{1}^{st}\left(⟨\Re \left({F}\left({u}\right)\right),\Im \left({F}\left({u}\right)\right)⟩\right)=\Re \left({F}\left({u}\right)\right)$
40 36 39 eqtrdi ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {1}^{st}\left({u}\right)=\Re \left({F}\left({u}\right)\right)$
41 40 fveq2d ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left|{1}^{st}\left({u}\right)\right|=\left|\Re \left({F}\left({u}\right)\right)\right|$
42 absrele ${⊢}{F}\left({u}\right)\in ℂ\to \left|\Re \left({F}\left({u}\right)\right)\right|\le \left|{F}\left({u}\right)\right|$
43 22 42 syl ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left|\Re \left({F}\left({u}\right)\right)\right|\le \left|{F}\left({u}\right)\right|$
44 41 43 eqbrtrd ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left|{1}^{st}\left({u}\right)\right|\le \left|{F}\left({u}\right)\right|$
45 fveq2 ${⊢}{z}={F}\left({u}\right)\to \left|{z}\right|=\left|{F}\left({u}\right)\right|$
46 45 breq1d ${⊢}{z}={F}\left({u}\right)\to \left(\left|{z}\right|\le {R}↔\left|{F}\left({u}\right)\right|\le {R}\right)$
47 simplrr ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}$
48 46 47 21 rspcdva ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left|{F}\left({u}\right)\right|\le {R}$
49 15 23 24 44 48 letrd ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left|{1}^{st}\left({u}\right)\right|\le {R}$
50 13 24 absled ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left(\left|{1}^{st}\left({u}\right)\right|\le {R}↔\left(-{R}\le {1}^{st}\left({u}\right)\wedge {1}^{st}\left({u}\right)\le {R}\right)\right)$
51 49 50 mpbid ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left(-{R}\le {1}^{st}\left({u}\right)\wedge {1}^{st}\left({u}\right)\le {R}\right)$
52 51 simpld ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to -{R}\le {1}^{st}\left({u}\right)$
53 51 simprd ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {1}^{st}\left({u}\right)\le {R}$
54 renegcl ${⊢}{R}\in ℝ\to -{R}\in ℝ$
55 24 54 syl ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to -{R}\in ℝ$
56 elicc2 ${⊢}\left(-{R}\in ℝ\wedge {R}\in ℝ\right)\to \left({1}^{st}\left({u}\right)\in \left[-{R},{R}\right]↔\left({1}^{st}\left({u}\right)\in ℝ\wedge -{R}\le {1}^{st}\left({u}\right)\wedge {1}^{st}\left({u}\right)\le {R}\right)\right)$
57 55 24 56 syl2anc ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left({1}^{st}\left({u}\right)\in \left[-{R},{R}\right]↔\left({1}^{st}\left({u}\right)\in ℝ\wedge -{R}\le {1}^{st}\left({u}\right)\wedge {1}^{st}\left({u}\right)\le {R}\right)\right)$
58 13 52 53 57 mpbir3and ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {1}^{st}\left({u}\right)\in \left[-{R},{R}\right]$
59 xp2nd ${⊢}{u}\in {ℝ}^{2}\to {2}^{nd}\left({u}\right)\in ℝ$
60 59 ad2antrl ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {2}^{nd}\left({u}\right)\in ℝ$
61 60 recnd ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {2}^{nd}\left({u}\right)\in ℂ$
62 61 abscld ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left|{2}^{nd}\left({u}\right)\right|\in ℝ$
63 35 fveq2d ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {2}^{nd}\left({u}\right)={2}^{nd}\left(⟨\Re \left({F}\left({u}\right)\right),\Im \left({F}\left({u}\right)\right)⟩\right)$
64 37 38 op2nd ${⊢}{2}^{nd}\left(⟨\Re \left({F}\left({u}\right)\right),\Im \left({F}\left({u}\right)\right)⟩\right)=\Im \left({F}\left({u}\right)\right)$
65 63 64 eqtrdi ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {2}^{nd}\left({u}\right)=\Im \left({F}\left({u}\right)\right)$
66 65 fveq2d ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left|{2}^{nd}\left({u}\right)\right|=\left|\Im \left({F}\left({u}\right)\right)\right|$
67 absimle ${⊢}{F}\left({u}\right)\in ℂ\to \left|\Im \left({F}\left({u}\right)\right)\right|\le \left|{F}\left({u}\right)\right|$
68 22 67 syl ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left|\Im \left({F}\left({u}\right)\right)\right|\le \left|{F}\left({u}\right)\right|$
69 66 68 eqbrtrd ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left|{2}^{nd}\left({u}\right)\right|\le \left|{F}\left({u}\right)\right|$
70 62 23 24 69 48 letrd ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left|{2}^{nd}\left({u}\right)\right|\le {R}$
71 60 24 absled ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left(\left|{2}^{nd}\left({u}\right)\right|\le {R}↔\left(-{R}\le {2}^{nd}\left({u}\right)\wedge {2}^{nd}\left({u}\right)\le {R}\right)\right)$
72 70 71 mpbid ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left(-{R}\le {2}^{nd}\left({u}\right)\wedge {2}^{nd}\left({u}\right)\le {R}\right)$
73 72 simpld ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to -{R}\le {2}^{nd}\left({u}\right)$
74 72 simprd ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {2}^{nd}\left({u}\right)\le {R}$
75 elicc2 ${⊢}\left(-{R}\in ℝ\wedge {R}\in ℝ\right)\to \left({2}^{nd}\left({u}\right)\in \left[-{R},{R}\right]↔\left({2}^{nd}\left({u}\right)\in ℝ\wedge -{R}\le {2}^{nd}\left({u}\right)\wedge {2}^{nd}\left({u}\right)\le {R}\right)\right)$
76 55 24 75 syl2anc ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to \left({2}^{nd}\left({u}\right)\in \left[-{R},{R}\right]↔\left({2}^{nd}\left({u}\right)\in ℝ\wedge -{R}\le {2}^{nd}\left({u}\right)\wedge {2}^{nd}\left({u}\right)\le {R}\right)\right)$
77 60 73 74 76 mpbir3and ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {2}^{nd}\left({u}\right)\in \left[-{R},{R}\right]$
78 58 77 opelxpd ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to ⟨{1}^{st}\left({u}\right),{2}^{nd}\left({u}\right)⟩\in \left(\left[-{R},{R}\right]×\left[-{R},{R}\right]\right)$
79 11 78 eqeltrd ${⊢}\left(\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\wedge \left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\right)\to {u}\in \left(\left[-{R},{R}\right]×\left[-{R},{R}\right]\right)$
80 79 ex ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to \left(\left({u}\in {ℝ}^{2}\wedge {F}\left({u}\right)\in {X}\right)\to {u}\in \left(\left[-{R},{R}\right]×\left[-{R},{R}\right]\right)\right)$
81 9 80 syl5bi ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to \left({u}\in {{F}}^{-1}\left[{X}\right]\to {u}\in \left(\left[-{R},{R}\right]×\left[-{R},{R}\right]\right)\right)$
82 81 ssrdv ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to {{F}}^{-1}\left[{X}\right]\subseteq \left[-{R},{R}\right]×\left[-{R},{R}\right]$
83 f1ofun ${⊢}{F}:{ℝ}^{2}\underset{1-1 onto}{⟶}ℂ\to \mathrm{Fun}{F}$
84 6 83 ax-mp ${⊢}\mathrm{Fun}{F}$
85 f1ofo ${⊢}{F}:{ℝ}^{2}\underset{1-1 onto}{⟶}ℂ\to {F}:{ℝ}^{2}\underset{onto}{⟶}ℂ$
86 forn ${⊢}{F}:{ℝ}^{2}\underset{onto}{⟶}ℂ\to \mathrm{ran}{F}=ℂ$
87 6 85 86 mp2b ${⊢}\mathrm{ran}{F}=ℂ$
88 19 87 sseqtrrdi ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to {X}\subseteq \mathrm{ran}{F}$
89 funimass1 ${⊢}\left(\mathrm{Fun}{F}\wedge {X}\subseteq \mathrm{ran}{F}\right)\to \left({{F}}^{-1}\left[{X}\right]\subseteq \left[-{R},{R}\right]×\left[-{R},{R}\right]\to {X}\subseteq {F}\left[\left[-{R},{R}\right]×\left[-{R},{R}\right]\right]\right)$
90 84 88 89 sylancr ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to \left({{F}}^{-1}\left[{X}\right]\subseteq \left[-{R},{R}\right]×\left[-{R},{R}\right]\to {X}\subseteq {F}\left[\left[-{R},{R}\right]×\left[-{R},{R}\right]\right]\right)$
91 82 90 mpd ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to {X}\subseteq {F}\left[\left[-{R},{R}\right]×\left[-{R},{R}\right]\right]$
92 91 4 sseqtrrdi ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to {X}\subseteq {Y}$
93 eqid ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
94 3 93 1 cnrehmeo ${⊢}{F}\in \left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\mathrm{Homeo}{J}\right)$
95 imaexg ${⊢}{F}\in \left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\mathrm{Homeo}{J}\right)\to {F}\left[\left[-{R},{R}\right]×\left[-{R},{R}\right]\right]\in \mathrm{V}$
96 94 95 ax-mp ${⊢}{F}\left[\left[-{R},{R}\right]×\left[-{R},{R}\right]\right]\in \mathrm{V}$
97 4 96 eqeltri ${⊢}{Y}\in \mathrm{V}$
98 97 a1i ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to {Y}\in \mathrm{V}$
99 restabs ${⊢}\left({J}\in \mathrm{Top}\wedge {X}\subseteq {Y}\wedge {Y}\in \mathrm{V}\right)\to \left({J}{↾}_{𝑡}{Y}\right){↾}_{𝑡}{X}={J}{↾}_{𝑡}{X}$
100 5 92 98 99 mp3an2i ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to \left({J}{↾}_{𝑡}{Y}\right){↾}_{𝑡}{X}={J}{↾}_{𝑡}{X}$
101 100 2 eqtr4di ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to \left({J}{↾}_{𝑡}{Y}\right){↾}_{𝑡}{X}={T}$
102 4 oveq2i ${⊢}{J}{↾}_{𝑡}{Y}={J}{↾}_{𝑡}{F}\left[\left[-{R},{R}\right]×\left[-{R},{R}\right]\right]$
103 ishmeo ${⊢}{F}\in \left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\mathrm{Homeo}{J}\right)↔\left({F}\in \left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\mathrm{Cn}{J}\right)\wedge {{F}}^{-1}\in \left({J}\mathrm{Cn}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)$
104 94 103 mpbi ${⊢}\left({F}\in \left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\mathrm{Cn}{J}\right)\wedge {{F}}^{-1}\in \left({J}\mathrm{Cn}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)$
105 104 simpli ${⊢}{F}\in \left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\mathrm{Cn}{J}\right)$
106 iccssre ${⊢}\left(-{R}\in ℝ\wedge {R}\in ℝ\right)\to \left[-{R},{R}\right]\subseteq ℝ$
107 54 106 mpancom ${⊢}{R}\in ℝ\to \left[-{R},{R}\right]\subseteq ℝ$
108 1 93 rerest ${⊢}\left[-{R},{R}\right]\subseteq ℝ\to {J}{↾}_{𝑡}\left[-{R},{R}\right]=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[-{R},{R}\right]$
109 107 108 syl ${⊢}{R}\in ℝ\to {J}{↾}_{𝑡}\left[-{R},{R}\right]=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[-{R},{R}\right]$
110 109 109 oveq12d ${⊢}{R}\in ℝ\to \left({J}{↾}_{𝑡}\left[-{R},{R}\right]\right){×}_{t}\left({J}{↾}_{𝑡}\left[-{R},{R}\right]\right)=\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[-{R},{R}\right]\right){×}_{t}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[-{R},{R}\right]\right)$
111 retop ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
112 ovex ${⊢}\left[-{R},{R}\right]\in \mathrm{V}$
113 txrest ${⊢}\left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\right)\wedge \left(\left[-{R},{R}\right]\in \mathrm{V}\wedge \left[-{R},{R}\right]\in \mathrm{V}\right)\right)\to \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right){↾}_{𝑡}\left(\left[-{R},{R}\right]×\left[-{R},{R}\right]\right)=\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[-{R},{R}\right]\right){×}_{t}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[-{R},{R}\right]\right)$
114 111 111 112 112 113 mp4an ${⊢}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right){↾}_{𝑡}\left(\left[-{R},{R}\right]×\left[-{R},{R}\right]\right)=\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[-{R},{R}\right]\right){×}_{t}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[-{R},{R}\right]\right)$
115 110 114 eqtr4di ${⊢}{R}\in ℝ\to \left({J}{↾}_{𝑡}\left[-{R},{R}\right]\right){×}_{t}\left({J}{↾}_{𝑡}\left[-{R},{R}\right]\right)=\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right){↾}_{𝑡}\left(\left[-{R},{R}\right]×\left[-{R},{R}\right]\right)$
116 eqid ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[-{R},{R}\right]=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[-{R},{R}\right]$
117 93 116 icccmp ${⊢}\left(-{R}\in ℝ\wedge {R}\in ℝ\right)\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[-{R},{R}\right]\in \mathrm{Comp}$
118 54 117 mpancom ${⊢}{R}\in ℝ\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[-{R},{R}\right]\in \mathrm{Comp}$
119 109 118 eqeltrd ${⊢}{R}\in ℝ\to {J}{↾}_{𝑡}\left[-{R},{R}\right]\in \mathrm{Comp}$
120 txcmp ${⊢}\left({J}{↾}_{𝑡}\left[-{R},{R}\right]\in \mathrm{Comp}\wedge {J}{↾}_{𝑡}\left[-{R},{R}\right]\in \mathrm{Comp}\right)\to \left({J}{↾}_{𝑡}\left[-{R},{R}\right]\right){×}_{t}\left({J}{↾}_{𝑡}\left[-{R},{R}\right]\right)\in \mathrm{Comp}$
121 119 119 120 syl2anc ${⊢}{R}\in ℝ\to \left({J}{↾}_{𝑡}\left[-{R},{R}\right]\right){×}_{t}\left({J}{↾}_{𝑡}\left[-{R},{R}\right]\right)\in \mathrm{Comp}$
122 115 121 eqeltrrd ${⊢}{R}\in ℝ\to \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right){↾}_{𝑡}\left(\left[-{R},{R}\right]×\left[-{R},{R}\right]\right)\in \mathrm{Comp}$
123 imacmp ${⊢}\left({F}\in \left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\mathrm{Cn}{J}\right)\wedge \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){×}_{t}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right){↾}_{𝑡}\left(\left[-{R},{R}\right]×\left[-{R},{R}\right]\right)\in \mathrm{Comp}\right)\to {J}{↾}_{𝑡}{F}\left[\left[-{R},{R}\right]×\left[-{R},{R}\right]\right]\in \mathrm{Comp}$
124 105 122 123 sylancr ${⊢}{R}\in ℝ\to {J}{↾}_{𝑡}{F}\left[\left[-{R},{R}\right]×\left[-{R},{R}\right]\right]\in \mathrm{Comp}$
125 102 124 eqeltrid ${⊢}{R}\in ℝ\to {J}{↾}_{𝑡}{Y}\in \mathrm{Comp}$
126 125 ad2antrl ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to {J}{↾}_{𝑡}{Y}\in \mathrm{Comp}$
127 imassrn ${⊢}{F}\left[\left[-{R},{R}\right]×\left[-{R},{R}\right]\right]\subseteq \mathrm{ran}{F}$
128 4 127 eqsstri ${⊢}{Y}\subseteq \mathrm{ran}{F}$
129 f1of ${⊢}{F}:{ℝ}^{2}\underset{1-1 onto}{⟶}ℂ\to {F}:{ℝ}^{2}⟶ℂ$
130 frn ${⊢}{F}:{ℝ}^{2}⟶ℂ\to \mathrm{ran}{F}\subseteq ℂ$
131 6 129 130 mp2b ${⊢}\mathrm{ran}{F}\subseteq ℂ$
132 128 131 sstri ${⊢}{Y}\subseteq ℂ$
133 simpl ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to {X}\in \mathrm{Clsd}\left({J}\right)$
134 17 restcldi ${⊢}\left({Y}\subseteq ℂ\wedge {X}\in \mathrm{Clsd}\left({J}\right)\wedge {X}\subseteq {Y}\right)\to {X}\in \mathrm{Clsd}\left({J}{↾}_{𝑡}{Y}\right)$
135 132 133 92 134 mp3an2i ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to {X}\in \mathrm{Clsd}\left({J}{↾}_{𝑡}{Y}\right)$
136 cmpcld ${⊢}\left({J}{↾}_{𝑡}{Y}\in \mathrm{Comp}\wedge {X}\in \mathrm{Clsd}\left({J}{↾}_{𝑡}{Y}\right)\right)\to \left({J}{↾}_{𝑡}{Y}\right){↾}_{𝑡}{X}\in \mathrm{Comp}$
137 126 135 136 syl2anc ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to \left({J}{↾}_{𝑡}{Y}\right){↾}_{𝑡}{X}\in \mathrm{Comp}$
138 101 137 eqeltrrd ${⊢}\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \left({R}\in ℝ\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left|{z}\right|\le {R}\right)\right)\to {T}\in \mathrm{Comp}$