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	⊢ ( ℂfld ↾s ℚ ) = ( ℂfld ↾s ℚ )
21		qqtopn	⊢ ( ( TopOpen ‘ ℝfld ) ↾t ℚ ) = ( TopOpen ‘ ( ℂfld ↾s ℚ ) )
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 ‘ 𝑅 ) ‘ 𝑄 ) )