Metamath Proof Explorer

Theorem rrhval

Description: Value of the canonical homormorphism from the real numbers to a complete space. (Contributed by Thierry Arnoux, 2-Nov-2017)

Ref Expression
Hypotheses rrhval.1 
|- J = ( topGen ` ran (,) )
rrhval.2 
|- K = ( TopOpen ` R )
Assertion rrhval 
|- ( R e. V -> ( RRHom ` R ) = ( ( J CnExt K ) ` ( QQHom ` R ) ) )

Proof

Step Hyp Ref Expression
1 rrhval.1 
 |-  J = ( topGen ` ran (,) )
2 rrhval.2 
 |-  K = ( TopOpen ` R )
3 elex 
 |-  ( R e. V -> R e. _V )
4 1 eqcomi 
 |-  ( topGen ` ran (,) ) = J
5 4 a1i 
 |-  ( r = R -> ( topGen ` ran (,) ) = J )
6 fveq2 
 |-  ( r = R -> ( TopOpen ` r ) = ( TopOpen ` R ) )
7 6 2 eqtr4di 
 |-  ( r = R -> ( TopOpen ` r ) = K )
8 5 7 oveq12d 
 |-  ( r = R -> ( ( topGen ` ran (,) ) CnExt ( TopOpen ` r ) ) = ( J CnExt K ) )
9 fveq2 
 |-  ( r = R -> ( QQHom ` r ) = ( QQHom ` R ) )
10 8 9 fveq12d 
 |-  ( r = R -> ( ( ( topGen ` ran (,) ) CnExt ( TopOpen ` r ) ) ` ( QQHom ` r ) ) = ( ( J CnExt K ) ` ( QQHom ` R ) ) )
11 df-rrh 
 |-  RRHom = ( r e. _V |-> ( ( ( topGen ` ran (,) ) CnExt ( TopOpen ` r ) ) ` ( QQHom ` r ) ) )
12 fvex 
 |-  ( ( J CnExt K ) ` ( QQHom ` R ) ) e. _V
13 10 11 12 fvmpt 
 |-  ( R e. _V -> ( RRHom ` R ) = ( ( J CnExt K ) ` ( QQHom ` R ) ) )
14 3 13 syl 
 |-  ( R e. V -> ( RRHom ` R ) = ( ( J CnExt K ) ` ( QQHom ` R ) ) )