Metamath Proof Explorer

Theorem gg-cnrehmeo

Description: The canonical bijection from ( RR X. RR ) to CC described in cnref1o is in fact a homeomorphism of the usual topologies on these sets. (It is also an isometry, if ( RR X. RR ) is metrized with the l2 norm.) (Contributed by Mario Carneiro, 25-Aug-2014) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses gg-cnrehmeo.1 
|- F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
gg-cnrehmeo.2 
|- J = ( topGen ` ran (,) )
gg-cnrehmeo.3 
|- K = ( TopOpen ` CCfld )
Assertion gg-cnrehmeo 
|- F e. ( ( J tX J ) Homeo K )

Proof

Step Hyp Ref Expression
1 gg-cnrehmeo.1 
 |-  F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
2 gg-cnrehmeo.2 
 |-  J = ( topGen ` ran (,) )
3 gg-cnrehmeo.3 
 |-  K = ( TopOpen ` CCfld )
4 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
5 2 4 eqeltri 
 |-  J e. ( TopOn ` RR )
6 5 a1i 
 |-  ( T. -> J e. ( TopOn ` RR ) )
7 3 cnfldtop 
 |-  K e. Top
8 cnrest2r 
 |-  ( K e. Top -> ( ( J tX J ) Cn ( K |`t RR ) ) C_ ( ( J tX J ) Cn K ) )
9 7 8 mp1i 
 |-  ( T. -> ( ( J tX J ) Cn ( K |`t RR ) ) C_ ( ( J tX J ) Cn K ) )
10 6 6 cnmpt1st 
 |-  ( T. -> ( x e. RR , y e. RR |-> x ) e. ( ( J tX J ) Cn J ) )
11 3 tgioo2 
 |-  ( topGen ` ran (,) ) = ( K |`t RR )
12 2 11 eqtri 
 |-  J = ( K |`t RR )
13 12 oveq2i 
 |-  ( ( J tX J ) Cn J ) = ( ( J tX J ) Cn ( K |`t RR ) )
14 10 13 eleqtrdi 
 |-  ( T. -> ( x e. RR , y e. RR |-> x ) e. ( ( J tX J ) Cn ( K |`t RR ) ) )
15 9 14 sseldd 
 |-  ( T. -> ( x e. RR , y e. RR |-> x ) e. ( ( J tX J ) Cn K ) )
16 3 cnfldtopon 
 |-  K e. ( TopOn ` CC )
17 16 a1i 
 |-  ( T. -> K e. ( TopOn ` CC ) )
18 ax-icn 
 |-  _i e. CC
19 18 a1i 
 |-  ( T. -> _i e. CC )
20 6 6 17 19 cnmpt2c 
 |-  ( T. -> ( x e. RR , y e. RR |-> _i ) e. ( ( J tX J ) Cn K ) )
21 6 6 cnmpt2nd 
 |-  ( T. -> ( x e. RR , y e. RR |-> y ) e. ( ( J tX J ) Cn J ) )
22 21 13 eleqtrdi 
 |-  ( T. -> ( x e. RR , y e. RR |-> y ) e. ( ( J tX J ) Cn ( K |`t RR ) ) )
23 9 22 sseldd 
 |-  ( T. -> ( x e. RR , y e. RR |-> y ) e. ( ( J tX J ) Cn K ) )
24 3 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( K tX K ) Cn K )
25 24 a1i 
 |-  ( T. -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( K tX K ) Cn K ) )
26 oveq12 
 |-  ( ( u = _i /\ v = y ) -> ( u x. v ) = ( _i x. y ) )
27 6 6 20 23 17 17 25 26 cnmpt22 
 |-  ( T. -> ( x e. RR , y e. RR |-> ( _i x. y ) ) e. ( ( J tX J ) Cn K ) )
28 3 addcn 
 |-  + e. ( ( K tX K ) Cn K )
29 28 a1i 
 |-  ( T. -> + e. ( ( K tX K ) Cn K ) )
30 6 6 15 27 29 cnmpt22f 
 |-  ( T. -> ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) ) e. ( ( J tX J ) Cn K ) )
31 1 30 eqeltrid 
 |-  ( T. -> F e. ( ( J tX J ) Cn K ) )
32 1 cnrecnv 
 |-  `' F = ( z e. CC |-> <. ( Re ` z ) , ( Im ` z ) >. )
33 ref 
 |-  Re : CC --> RR
34 33 a1i 
 |-  ( T. -> Re : CC --> RR )
35 34 feqmptd 
 |-  ( T. -> Re = ( z e. CC |-> ( Re ` z ) ) )
36 recncf 
 |-  Re e. ( CC -cn-> RR )
37 ssid 
 |-  CC C_ CC
38 ax-resscn 
 |-  RR C_ CC
39 16 toponrestid 
 |-  K = ( K |`t CC )
40 3 39 12 cncfcn 
 |-  ( ( CC C_ CC /\ RR C_ CC ) -> ( CC -cn-> RR ) = ( K Cn J ) )
41 37 38 40 mp2an 
 |-  ( CC -cn-> RR ) = ( K Cn J )
42 36 41 eleqtri 
 |-  Re e. ( K Cn J )
43 35 42 eqeltrrdi 
 |-  ( T. -> ( z e. CC |-> ( Re ` z ) ) e. ( K Cn J ) )
44 imf 
 |-  Im : CC --> RR
45 44 a1i 
 |-  ( T. -> Im : CC --> RR )
46 45 feqmptd 
 |-  ( T. -> Im = ( z e. CC |-> ( Im ` z ) ) )
47 imcncf 
 |-  Im e. ( CC -cn-> RR )
48 47 41 eleqtri 
 |-  Im e. ( K Cn J )
49 46 48 eqeltrrdi 
 |-  ( T. -> ( z e. CC |-> ( Im ` z ) ) e. ( K Cn J ) )
50 17 43 49 cnmpt1t 
 |-  ( T. -> ( z e. CC |-> <. ( Re ` z ) , ( Im ` z ) >. ) e. ( K Cn ( J tX J ) ) )
51 32 50 eqeltrid 
 |-  ( T. -> `' F e. ( K Cn ( J tX J ) ) )
52 ishmeo 
 |-  ( F e. ( ( J tX J ) Homeo K ) <-> ( F e. ( ( J tX J ) Cn K ) /\ `' F e. ( K Cn ( J tX J ) ) ) )
53 31 51 52 sylanbrc 
 |-  ( T. -> F e. ( ( J tX J ) Homeo K ) )
54 53 mptru 
 |-  F e. ( ( J tX J ) Homeo K )