Metamath Proof Explorer


Theorem rrhqima

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

Ref Expression
Assertion rrhqima ( ( 𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ ) → ( ( ℝHom ‘ 𝑅 ) ‘ 𝑄 ) = ( ( ℚHom ‘ 𝑅 ) ‘ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 eqid ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
2 eqid ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
3 1 2 rrhval ( 𝑅 ∈ ℝExt → ( ℝHom ‘ 𝑅 ) = ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑅 ) ) ‘ ( ℚHom ‘ 𝑅 ) ) )
4 3 fveq1d ( 𝑅 ∈ ℝExt → ( ( ℝHom ‘ 𝑅 ) ‘ 𝑄 ) = ( ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑅 ) ) ‘ ( ℚHom ‘ 𝑅 ) ) ‘ 𝑄 ) )
5 4 adantr ( ( 𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ ) → ( ( ℝHom ‘ 𝑅 ) ‘ 𝑄 ) = ( ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑅 ) ) ‘ ( ℚHom ‘ 𝑅 ) ) ‘ 𝑄 ) )
6 uniretop ℝ = ( topGen ‘ ran (,) )
7 eqid ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
8 retop ( topGen ‘ ran (,) ) ∈ Top
9 8 a1i ( ( 𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ ) → ( topGen ‘ ran (,) ) ∈ Top )
10 2 rrexthaus ( 𝑅 ∈ ℝExt → ( TopOpen ‘ 𝑅 ) ∈ Haus )
11 10 adantr ( ( 𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ ) → ( TopOpen ‘ 𝑅 ) ∈ Haus )
12 qssre ℚ ⊆ ℝ
13 12 a1i ( ( 𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ ) → ℚ ⊆ ℝ )
14 rrextnrg ( 𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing )
15 rrextdrg ( 𝑅 ∈ ℝExt → 𝑅 ∈ DivRing )
16 14 15 elind ( 𝑅 ∈ ℝExt → 𝑅 ∈ ( NrmRing ∩ DivRing ) )
17 eqid ( ℤMod ‘ 𝑅 ) = ( ℤMod ‘ 𝑅 )
18 17 rrextnlm ( 𝑅 ∈ ℝExt → ( ℤMod ‘ 𝑅 ) ∈ NrmMod )
19 rrextchr ( 𝑅 ∈ ℝExt → ( chr ‘ 𝑅 ) = 0 )
20 eqid ( ℂflds ℚ ) = ( ℂflds ℚ )
21 qqtopn ( ( TopOpen ‘ ℝfld ) ↾t ℚ ) = ( TopOpen ‘ ( ℂflds ℚ ) )
22 20 21 17 2 qqhcn ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ ( ℤMod ‘ 𝑅 ) ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) ∈ ( ( ( TopOpen ‘ ℝfld ) ↾t ℚ ) Cn ( TopOpen ‘ 𝑅 ) ) )
23 16 18 19 22 syl3anc ( 𝑅 ∈ ℝExt → ( ℚHom ‘ 𝑅 ) ∈ ( ( ( TopOpen ‘ ℝfld ) ↾t ℚ ) Cn ( TopOpen ‘ 𝑅 ) ) )
24 retopn ( topGen ‘ ran (,) ) = ( TopOpen ‘ ℝfld )
25 24 eqcomi ( TopOpen ‘ ℝfld ) = ( topGen ‘ ran (,) )
26 25 oveq1i ( ( TopOpen ‘ ℝfld ) ↾t ℚ ) = ( ( topGen ‘ ran (,) ) ↾t ℚ )
27 26 oveq1i ( ( ( TopOpen ‘ ℝfld ) ↾t ℚ ) Cn ( TopOpen ‘ 𝑅 ) ) = ( ( ( topGen ‘ ran (,) ) ↾t ℚ ) Cn ( TopOpen ‘ 𝑅 ) )
28 23 27 eleqtrdi ( 𝑅 ∈ ℝExt → ( ℚHom ‘ 𝑅 ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ℚ ) Cn ( TopOpen ‘ 𝑅 ) ) )
29 28 adantr ( ( 𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ ) → ( ℚHom ‘ 𝑅 ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ℚ ) Cn ( TopOpen ‘ 𝑅 ) ) )
30 simpr ( ( 𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ ) → 𝑄 ∈ ℚ )
31 6 7 9 11 13 29 30 cnextfres ( ( 𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ ) → ( ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑅 ) ) ‘ ( ℚHom ‘ 𝑅 ) ) ‘ 𝑄 ) = ( ( ℚHom ‘ 𝑅 ) ‘ 𝑄 ) )
32 5 31 eqtrd ( ( 𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ ) → ( ( ℝHom ‘ 𝑅 ) ‘ 𝑄 ) = ( ( ℚHom ‘ 𝑅 ) ‘ 𝑄 ) )