Metamath Proof Explorer

Theorem rrhre

Description: The RRHom homomorphism for the real numbers structure is the identity. (Contributed by Thierry Arnoux, 22-Oct-2017)

Ref Expression
Assertion rrhre 
|- ( RRHom ` RRfld ) = ( _I |` RR )

Proof

Step Hyp Ref Expression
1 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
2 rehaus 
 |-  ( topGen ` ran (,) ) e. Haus
3 2 a1i 
 |-  ( T. -> ( topGen ` ran (,) ) e. Haus )
4 rerrext 
 |-  RRfld e. RRExt
5 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
6 retopn 
 |-  ( topGen ` ran (,) ) = ( TopOpen ` RRfld )
7 5 6 rrhcne 
 |-  ( RRfld e. RRExt -> ( RRHom ` RRfld ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
8 4 7 mp1i 
 |-  ( T. -> ( RRHom ` RRfld ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
9 retop 
 |-  ( topGen ` ran (,) ) e. Top
10 1 toptopon 
 |-  ( ( topGen ` ran (,) ) e. Top <-> ( topGen ` ran (,) ) e. ( TopOn ` RR ) )
11 9 10 mpbi 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
12 idcn 
 |-  ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) -> ( _I |` RR ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
13 11 12 ax-mp 
 |-  ( _I |` RR ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) )
14 13 a1i 
 |-  ( T. -> ( _I |` RR ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
15 9 a1i 
 |-  ( T. -> ( topGen ` ran (,) ) e. Top )
16 f1oi 
 |-  ( _I |` QQ ) : QQ -1-1-onto-> QQ
17 f1of 
 |-  ( ( _I |` QQ ) : QQ -1-1-onto-> QQ -> ( _I |` QQ ) : QQ --> QQ )
18 16 17 ax-mp 
 |-  ( _I |` QQ ) : QQ --> QQ
19 qssre 
 |-  QQ C_ RR
20 fss 
 |-  ( ( ( _I |` QQ ) : QQ --> QQ /\ QQ C_ RR ) -> ( _I |` QQ ) : QQ --> RR )
21 18 19 20 mp2an 
 |-  ( _I |` QQ ) : QQ --> RR
22 21 a1i 
 |-  ( T. -> ( _I |` QQ ) : QQ --> RR )
23 19 a1i 
 |-  ( T. -> QQ C_ RR )
24 qdensere 
 |-  ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = RR
25 24 a1i 
 |-  ( T. -> ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = RR )
26 9 a1i 
 |-  ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> ( topGen ` ran (,) ) e. Top )
27 simplr 
 |-  ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> a e. ( topGen ` ran (,) ) )
28 simpr 
 |-  ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> x e. a )
29 opnneip 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ a e. ( topGen ` ran (,) ) /\ x e. a ) -> a e. ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) )
30 26 27 28 29 syl3anc 
 |-  ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> a e. ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) )
31 fvex 
 |-  ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) e. _V
32 qex 
 |-  QQ e. _V
33 elrestr 
 |-  ( ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) e. _V /\ QQ e. _V /\ a e. ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) ) -> ( a i^i QQ ) e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) )
34 31 32 33 mp3an12 
 |-  ( a e. ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) -> ( a i^i QQ ) e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) )
35 30 34 syl 
 |-  ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> ( a i^i QQ ) e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) )
36 inss2 
 |-  ( a i^i QQ ) C_ QQ
37 resiima 
 |-  ( ( a i^i QQ ) C_ QQ -> ( ( _I |` QQ ) " ( a i^i QQ ) ) = ( a i^i QQ ) )
38 36 37 ax-mp 
 |-  ( ( _I |` QQ ) " ( a i^i QQ ) ) = ( a i^i QQ )
39 inss1 
 |-  ( a i^i QQ ) C_ a
40 38 39 eqsstri 
 |-  ( ( _I |` QQ ) " ( a i^i QQ ) ) C_ a
41 40 a1i 
 |-  ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> ( ( _I |` QQ ) " ( a i^i QQ ) ) C_ a )
42 imaeq2 
 |-  ( b = ( a i^i QQ ) -> ( ( _I |` QQ ) " b ) = ( ( _I |` QQ ) " ( a i^i QQ ) ) )
43 42 sseq1d 
 |-  ( b = ( a i^i QQ ) -> ( ( ( _I |` QQ ) " b ) C_ a <-> ( ( _I |` QQ ) " ( a i^i QQ ) ) C_ a ) )
44 43 rspcev 
 |-  ( ( ( a i^i QQ ) e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) /\ ( ( _I |` QQ ) " ( a i^i QQ ) ) C_ a ) -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ( ( _I |` QQ ) " b ) C_ a )
45 35 41 44 syl2anc 
 |-  ( ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) /\ x e. a ) -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ( ( _I |` QQ ) " b ) C_ a )
46 45 ex 
 |-  ( ( x e. RR /\ a e. ( topGen ` ran (,) ) ) -> ( x e. a -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ( ( _I |` QQ ) " b ) C_ a ) )
47 46 ralrimiva 
 |-  ( x e. RR -> A. a e. ( topGen ` ran (,) ) ( x e. a -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ( ( _I |` QQ ) " b ) C_ a ) )
48 47 ancli 
 |-  ( x e. RR -> ( x e. RR /\ A. a e. ( topGen ` ran (,) ) ( x e. a -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ( ( _I |` QQ ) " b ) C_ a ) ) )
49 24 eleq2i 
 |-  ( x e. ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) <-> x e. RR )
50 49 biimpri 
 |-  ( x e. RR -> x e. ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) )
51 trnei 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ QQ C_ RR /\ x e. RR ) -> ( x e. ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) <-> ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) e. ( Fil ` QQ ) ) )
52 11 19 51 mp3an12 
 |-  ( x e. RR -> ( x e. ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) <-> ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) e. ( Fil ` QQ ) ) )
53 50 52 mpbid 
 |-  ( x e. RR -> ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) e. ( Fil ` QQ ) )
54 isflf 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) e. ( Fil ` QQ ) /\ ( _I |` QQ ) : QQ --> RR ) -> ( x e. ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ) ` ( _I |` QQ ) ) <-> ( x e. RR /\ A. a e. ( topGen ` ran (,) ) ( x e. a -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ( ( _I |` QQ ) " b ) C_ a ) ) ) )
55 11 21 54 mp3an13 
 |-  ( ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) e. ( Fil ` QQ ) -> ( x e. ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ) ` ( _I |` QQ ) ) <-> ( x e. RR /\ A. a e. ( topGen ` ran (,) ) ( x e. a -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ( ( _I |` QQ ) " b ) C_ a ) ) ) )
56 53 55 syl 
 |-  ( x e. RR -> ( x e. ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ) ` ( _I |` QQ ) ) <-> ( x e. RR /\ A. a e. ( topGen ` ran (,) ) ( x e. a -> E. b e. ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ( ( _I |` QQ ) " b ) C_ a ) ) ) )
57 48 56 mpbird 
 |-  ( x e. RR -> x e. ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ) ` ( _I |` QQ ) ) )
58 57 ne0d 
 |-  ( x e. RR -> ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ) ` ( _I |` QQ ) ) =/= (/) )
59 58 adantl 
 |-  ( ( T. /\ x e. RR ) -> ( ( ( topGen ` ran (,) ) fLimf ( ( ( nei ` ( topGen ` ran (,) ) ) ` { x } ) |`t QQ ) ) ` ( _I |` QQ ) ) =/= (/) )
60 recusp 
 |-  RRfld e. CUnifSp
61 cuspusp 
 |-  ( RRfld e. CUnifSp -> RRfld e. UnifSp )
62 60 61 ax-mp 
 |-  RRfld e. UnifSp
63 6 uspreg 
 |-  ( ( RRfld e. UnifSp /\ ( topGen ` ran (,) ) e. Haus ) -> ( topGen ` ran (,) ) e. Reg )
64 62 2 63 mp2an 
 |-  ( topGen ` ran (,) ) e. Reg
65 64 a1i 
 |-  ( T. -> ( topGen ` ran (,) ) e. Reg )
66 resabs1 
 |-  ( QQ C_ RR -> ( ( _I |` RR ) |` QQ ) = ( _I |` QQ ) )
67 19 66 ax-mp 
 |-  ( ( _I |` RR ) |` QQ ) = ( _I |` QQ )
68 1 cnrest 
 |-  ( ( ( _I |` RR ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) /\ QQ C_ RR ) -> ( ( _I |` RR ) |` QQ ) e. ( ( ( topGen ` ran (,) ) |`t QQ ) Cn ( topGen ` ran (,) ) ) )
69 13 19 68 mp2an 
 |-  ( ( _I |` RR ) |` QQ ) e. ( ( ( topGen ` ran (,) ) |`t QQ ) Cn ( topGen ` ran (,) ) )
70 67 69 eqeltrri 
 |-  ( _I |` QQ ) e. ( ( ( topGen ` ran (,) ) |`t QQ ) Cn ( topGen ` ran (,) ) )
71 70 a1i 
 |-  ( T. -> ( _I |` QQ ) e. ( ( ( topGen ` ran (,) ) |`t QQ ) Cn ( topGen ` ran (,) ) ) )
72 1 1 15 3 22 23 25 59 65 71 cnextfres1 
 |-  ( T. -> ( ( ( ( topGen ` ran (,) ) CnExt ( topGen ` ran (,) ) ) ` ( _I |` QQ ) ) |` QQ ) = ( _I |` QQ ) )
73 72 mptru 
 |-  ( ( ( ( topGen ` ran (,) ) CnExt ( topGen ` ran (,) ) ) ` ( _I |` QQ ) ) |` QQ ) = ( _I |` QQ )
74 recms 
 |-  RRfld e. CMetSp
75 74 elexi 
 |-  RRfld e. _V
76 5 6 rrhval 
 |-  ( RRfld e. _V -> ( RRHom ` RRfld ) = ( ( ( topGen ` ran (,) ) CnExt ( topGen ` ran (,) ) ) ` ( QQHom ` RRfld ) ) )
77 75 76 ax-mp 
 |-  ( RRHom ` RRfld ) = ( ( ( topGen ` ran (,) ) CnExt ( topGen ` ran (,) ) ) ` ( QQHom ` RRfld ) )
78 qqhre 
 |-  ( QQHom ` RRfld ) = ( _I |` QQ )
79 78 fveq2i 
 |-  ( ( ( topGen ` ran (,) ) CnExt ( topGen ` ran (,) ) ) ` ( QQHom ` RRfld ) ) = ( ( ( topGen ` ran (,) ) CnExt ( topGen ` ran (,) ) ) ` ( _I |` QQ ) )
80 77 79 eqtri 
 |-  ( RRHom ` RRfld ) = ( ( ( topGen ` ran (,) ) CnExt ( topGen ` ran (,) ) ) ` ( _I |` QQ ) )
81 80 reseq1i 
 |-  ( ( RRHom ` RRfld ) |` QQ ) = ( ( ( ( topGen ` ran (,) ) CnExt ( topGen ` ran (,) ) ) ` ( _I |` QQ ) ) |` QQ )
82 73 81 67 3eqtr4i 
 |-  ( ( RRHom ` RRfld ) |` QQ ) = ( ( _I |` RR ) |` QQ )
83 82 a1i 
 |-  ( T. -> ( ( RRHom ` RRfld ) |` QQ ) = ( ( _I |` RR ) |` QQ ) )
84 1 3 8 14 83 23 25 hauseqcn 
 |-  ( T. -> ( RRHom ` RRfld ) = ( _I |` RR ) )
85 84 mptru 
 |-  ( RRHom ` RRfld ) = ( _I |` RR )