Metamath Proof Explorer

Theorem rrhqima

Description: The RRHom homomorphism leaves rational numbers unchanged. (Contributed by Thierry Arnoux, 27-Mar-2018)

Ref Expression
Assertion rrhqima 
|- ( ( R e. RRExt /\ Q e. QQ ) -> ( ( RRHom ` R ) ` Q ) = ( ( QQHom ` R ) ` Q ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
2 eqid 
 |-  ( TopOpen ` R ) = ( TopOpen ` R )
3 1 2 rrhval 
 |-  ( R e. RRExt -> ( RRHom ` R ) = ( ( ( topGen ` ran (,) ) CnExt ( TopOpen ` R ) ) ` ( QQHom ` R ) ) )
4 3 fveq1d 
 |-  ( R e. RRExt -> ( ( RRHom ` R ) ` Q ) = ( ( ( ( topGen ` ran (,) ) CnExt ( TopOpen ` R ) ) ` ( QQHom ` R ) ) ` Q ) )
5 4 adantr 
 |-  ( ( R e. RRExt /\ Q e. QQ ) -> ( ( RRHom ` R ) ` Q ) = ( ( ( ( topGen ` ran (,) ) CnExt ( TopOpen ` R ) ) ` ( QQHom ` R ) ) ` Q ) )
6 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
7 eqid 
 |-  U. ( TopOpen ` R ) = U. ( TopOpen ` R )
8 retop 
 |-  ( topGen ` ran (,) ) e. Top
9 8 a1i 
 |-  ( ( R e. RRExt /\ Q e. QQ ) -> ( topGen ` ran (,) ) e. Top )
10 2 rrexthaus 
 |-  ( R e. RRExt -> ( TopOpen ` R ) e. Haus )
11 10 adantr 
 |-  ( ( R e. RRExt /\ Q e. QQ ) -> ( TopOpen ` R ) e. Haus )
12 qssre 
 |-  QQ C_ RR
13 12 a1i 
 |-  ( ( R e. RRExt /\ Q e. QQ ) -> QQ C_ RR )
14 rrextnrg 
 |-  ( R e. RRExt -> R e. NrmRing )
15 rrextdrg 
 |-  ( R e. RRExt -> R e. DivRing )
16 14 15 elind 
 |-  ( R e. RRExt -> R e. ( NrmRing i^i DivRing ) )
17 eqid 
 |-  ( ZMod ` R ) = ( ZMod ` R )
18 17 rrextnlm 
 |-  ( R e. RRExt -> ( ZMod ` R ) e. NrmMod )
19 rrextchr 
 |-  ( R e. RRExt -> ( chr ` R ) = 0 )
20 eqid 
 |-  ( CCfld |`s QQ ) = ( CCfld |`s QQ )
21 qqtopn 
 |-  ( ( TopOpen ` RRfld ) |`t QQ ) = ( TopOpen ` ( CCfld |`s QQ ) )
22 20 21 17 2 qqhcn 
 |-  ( ( R e. ( NrmRing i^i DivRing ) /\ ( ZMod ` R ) e. NrmMod /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) e. ( ( ( TopOpen ` RRfld ) |`t QQ ) Cn ( TopOpen ` R ) ) )
23 16 18 19 22 syl3anc 
 |-  ( R e. RRExt -> ( QQHom ` R ) e. ( ( ( TopOpen ` RRfld ) |`t QQ ) Cn ( TopOpen ` R ) ) )
24 retopn 
 |-  ( topGen ` ran (,) ) = ( TopOpen ` RRfld )
25 24 eqcomi 
 |-  ( TopOpen ` RRfld ) = ( topGen ` ran (,) )
26 25 oveq1i 
 |-  ( ( TopOpen ` RRfld ) |`t QQ ) = ( ( topGen ` ran (,) ) |`t QQ )
27 26 oveq1i 
 |-  ( ( ( TopOpen ` RRfld ) |`t QQ ) Cn ( TopOpen ` R ) ) = ( ( ( topGen ` ran (,) ) |`t QQ ) Cn ( TopOpen ` R ) )
28 23 27 eleqtrdi 
 |-  ( R e. RRExt -> ( QQHom ` R ) e. ( ( ( topGen ` ran (,) ) |`t QQ ) Cn ( TopOpen ` R ) ) )
29 28 adantr 
 |-  ( ( R e. RRExt /\ Q e. QQ ) -> ( QQHom ` R ) e. ( ( ( topGen ` ran (,) ) |`t QQ ) Cn ( TopOpen ` R ) ) )
30 simpr 
 |-  ( ( R e. RRExt /\ Q e. QQ ) -> Q e. QQ )
31 6 7 9 11 13 29 30 cnextfres 
 |-  ( ( R e. RRExt /\ Q e. QQ ) -> ( ( ( ( topGen ` ran (,) ) CnExt ( TopOpen ` R ) ) ` ( QQHom ` R ) ) ` Q ) = ( ( QQHom ` R ) ` Q ) )
32 5 31 eqtrd 
 |-  ( ( R e. RRExt /\ Q e. QQ ) -> ( ( RRHom ` R ) ` Q ) = ( ( QQHom ` R ) ` Q ) )