rrhqima

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

		Ref	Expression
	Assertion	rrhqima	$⊢ (R \in ℝExt \land Q \in ℚ) \to ℝHom (R) (Q) = ℚHom (R) (Q)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
2		eqid	$⊢ TopOpen (R) = TopOpen (R)$
3	1 2	rrhval	$⊢ R \in ℝExt \to ℝHom (R) = (topGen (ran (.)) CnExt TopOpen (R)) (ℚHom (R))$
4	3	fveq1d	$⊢ R \in ℝExt \to ℝHom (R) (Q) = (topGen (ran (.)) CnExt TopOpen (R)) (ℚHom (R)) (Q)$
5	4	adantr	$⊢ (R \in ℝExt \land Q \in ℚ) \to ℝHom (R) (Q) = (topGen (ran (.)) CnExt TopOpen (R)) (ℚHom (R)) (Q)$
6		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
7		eqid	$⊢ ⋃ TopOpen (R) = ⋃ TopOpen (R)$
8		retop	$⊢ topGen (ran (.)) \in Top$
9	8	a1i	$⊢ (R \in ℝExt \land Q \in ℚ) \to topGen (ran (.)) \in Top$
10	2	rrexthaus	$⊢ R \in ℝExt \to TopOpen (R) \in Haus$
11	10	adantr	$⊢ (R \in ℝExt \land Q \in ℚ) \to TopOpen (R) \in Haus$
12		qssre	$⊢ ℚ \subseteq ℝ$
13	12	a1i	$⊢ (R \in ℝExt \land Q \in ℚ) \to ℚ \subseteq ℝ$
14		rrextnrg	$⊢ R \in ℝExt \to R \in NrmRing$
15		rrextdrg	$⊢ R \in ℝExt \to R \in DivRing$
16	14 15	elind	$⊢ R \in ℝExt \to R \in (NrmRing \cap DivRing)$
17		eqid	$⊢ ℤMod (R) = ℤMod (R)$
18	17	rrextnlm	$⊢ R \in ℝExt \to ℤMod (R) \in NrmMod$
19		rrextchr	$⊢ R \in ℝExt \to chr (R) = 0$
20		eqid	$⊢ ℂ_{fld} ↾_{𝑠} ℚ = ℂ_{fld} ↾_{𝑠} ℚ$
21		qqtopn	$⊢ TopOpen (ℝ_{fld}) ↾_{𝑡} ℚ = TopOpen (ℂ_{fld} ↾_{𝑠} ℚ)$
22	20 21 17 2	qqhcn	$⊢ (R \in (NrmRing \cap DivRing) \land ℤMod (R) \in NrmMod \land chr (R) = 0) \to ℚHom (R) \in ((TopOpen (ℝ_{fld}) ↾_{𝑡} ℚ) Cn TopOpen (R))$
23	16 18 19 22	syl3anc	$⊢ R \in ℝExt \to ℚHom (R) \in ((TopOpen (ℝ_{fld}) ↾_{𝑡} ℚ) Cn TopOpen (R))$
24		retopn	$⊢ topGen (ran (.)) = TopOpen (ℝ_{fld})$
25	24	eqcomi	$⊢ TopOpen (ℝ_{fld}) = topGen (ran (.))$
26	25	oveq1i	$⊢ TopOpen (ℝ_{fld}) ↾_{𝑡} ℚ = topGen (ran (.)) ↾_{𝑡} ℚ$
27	26	oveq1i	$⊢ (TopOpen (ℝ_{fld}) ↾_{𝑡} ℚ) Cn TopOpen (R) = (topGen (ran (.)) ↾_{𝑡} ℚ) Cn TopOpen (R)$
28	23 27	eleqtrdi	$⊢ R \in ℝExt \to ℚHom (R) \in ((topGen (ran (.)) ↾_{𝑡} ℚ) Cn TopOpen (R))$
29	28	adantr	$⊢ (R \in ℝExt \land Q \in ℚ) \to ℚHom (R) \in ((topGen (ran (.)) ↾_{𝑡} ℚ) Cn TopOpen (R))$
30		simpr	$⊢ (R \in ℝExt \land Q \in ℚ) \to Q \in ℚ$
31	6 7 9 11 13 29 30	cnextfres	$⊢ (R \in ℝExt \land Q \in ℚ) \to (topGen (ran (.)) CnExt TopOpen (R)) (ℚHom (R)) (Q) = ℚHom (R) (Q)$
32	5 31	eqtrd	$⊢ (R \in ℝExt \land Q \in ℚ) \to ℝHom (R) (Q) = ℚHom (R) (Q)$

Metamath Proof Explorer

Theorem rrhqima

Proof