Metamath Proof Explorer

Definition df-rrh

Description: Define the canonical homomorphism from the real numbers to any complete field, as the extension by continuity of the canonical homomorphism from the rational numbers. (Contributed by Mario Carneiro, 22-Oct-2017) (Revised by Thierry Arnoux, 23-Oct-2017)

Ref Expression
Assertion df-rrh 
|- RRHom = ( r e. _V |-> ( ( ( topGen ` ran (,) ) CnExt ( TopOpen ` r ) ) ` ( QQHom ` r ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crrh 
 |-  RRHom
1 vr 
 |-  r
2 cvv 
 |-  _V
3 ctg 
 |-  topGen
4 cioo 
 |-  (,)
5 4 crn 
 |-  ran (,)
6 5 3 cfv 
 |-  ( topGen ` ran (,) )
7 ccnext 
 |-  CnExt
8 ctopn 
 |-  TopOpen
9 1 cv 
 |-  r
10 9 8 cfv 
 |-  ( TopOpen ` r )
11 6 10 7 co 
 |-  ( ( topGen ` ran (,) ) CnExt ( TopOpen ` r ) )
12 cqqh 
 |-  QQHom
13 9 12 cfv 
 |-  ( QQHom ` r )
14 13 11 cfv 
 |-  ( ( ( topGen ` ran (,) ) CnExt ( TopOpen ` r ) ) ` ( QQHom ` r ) )
15 1 2 14 cmpt 
 |-  ( r e. _V |-> ( ( ( topGen ` ran (,) ) CnExt ( TopOpen ` r ) ) ` ( QQHom ` r ) ) )
16 0 15 wceq 
 |-  RRHom = ( r e. _V |-> ( ( ( topGen ` ran (,) ) CnExt ( TopOpen ` r ) ) ` ( QQHom ` r ) ) )