Metamath Proof Explorer

Theorem 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)

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

Proof

Step Hyp Ref Expression
1 cnrehmeo.1 
 |-  F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
2 cnrehmeo.2 
 |-  J = ( topGen ` ran (,) )
3 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 mulcn 
 |-  x. e. ( ( K tX K ) Cn K )
25 24 a1i 
 |-  ( T. -> x. e. ( ( K tX K ) Cn K ) )
26 6 6 20 23 25 cnmpt22f 
 |-  ( T. -> ( x e. RR , y e. RR |-> ( _i x. y ) ) e. ( ( J tX J ) Cn K ) )
27 3 addcn 
 |-  + e. ( ( K tX K ) Cn K )
28 27 a1i 
 |-  ( T. -> + e. ( ( K tX K ) Cn K ) )
29 6 6 15 26 28 cnmpt22f 
 |-  ( T. -> ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) ) e. ( ( J tX J ) Cn K ) )
30 1 29 eqeltrid 
 |-  ( T. -> F e. ( ( J tX J ) Cn K ) )
31 1 cnrecnv 
 |-  `' F = ( z e. CC |-> <. ( Re ` z ) , ( Im ` z ) >. )
32 ref 
 |-  Re : CC --> RR
33 32 a1i 
 |-  ( T. -> Re : CC --> RR )
34 33 feqmptd 
 |-  ( T. -> Re = ( z e. CC |-> ( Re ` z ) ) )
35 recncf 
 |-  Re e. ( CC -cn-> RR )
36 ssid 
 |-  CC C_ CC
37 ax-resscn 
 |-  RR C_ CC
38 16 toponrestid 
 |-  K = ( K |`t CC )
39 3 38 12 cncfcn 
 |-  ( ( CC C_ CC /\ RR C_ CC ) -> ( CC -cn-> RR ) = ( K Cn J ) )
40 36 37 39 mp2an 
 |-  ( CC -cn-> RR ) = ( K Cn J )
41 35 40 eleqtri 
 |-  Re e. ( K Cn J )
42 34 41 eqeltrrdi 
 |-  ( T. -> ( z e. CC |-> ( Re ` z ) ) e. ( K Cn J ) )
43 imf 
 |-  Im : CC --> RR
44 43 a1i 
 |-  ( T. -> Im : CC --> RR )
45 44 feqmptd 
 |-  ( T. -> Im = ( z e. CC |-> ( Im ` z ) ) )
46 imcncf 
 |-  Im e. ( CC -cn-> RR )
47 46 40 eleqtri 
 |-  Im e. ( K Cn J )
48 45 47 eqeltrrdi 
 |-  ( T. -> ( z e. CC |-> ( Im ` z ) ) e. ( K Cn J ) )
49 17 42 48 cnmpt1t 
 |-  ( T. -> ( z e. CC |-> <. ( Re ` z ) , ( Im ` z ) >. ) e. ( K Cn ( J tX J ) ) )
50 31 49 eqeltrid 
 |-  ( T. -> `' F e. ( K Cn ( J tX J ) ) )
51 ishmeo 
 |-  ( F e. ( ( J tX J ) Homeo K ) <-> ( F e. ( ( J tX J ) Cn K ) /\ `' F e. ( K Cn ( J tX J ) ) ) )
52 30 50 51 sylanbrc 
 |-  ( T. -> F e. ( ( J tX J ) Homeo K ) )
53 52 mptru 
 |-  F e. ( ( J tX J ) Homeo K )