Theorem rrhfe

Description: If R is an extension of RR , then the canonical homomorphism of RR into R is a function. (Contributed by Thierry Arnoux, 2-May-2018)

	Ref	Expression
Hypothesis	rrhfe.b	$$⊢B={\mathrm{Base}}_R$$
Assertion	rrhfe	$$⊢R\in \mathrm{ℝExt}\to \mathrm{ℝHom}\left(R\right):ℝ⟶B$$

Proof

Step	Hyp	Ref	Expression
1		rrhfe.b	$$⊢B={\mathrm{Base}}_R$$
2		eqid	$$⊢{\mathrm{dist}\left(R\right)\upharpoonright }_{\left(B\times B\right)}={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(B\times B\right)}$$
3		eqid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
4		eqid	$$⊢\mathrm{TopOpen}\left(R\right)=\mathrm{TopOpen}\left(R\right)$$
5		eqid	$$⊢\mathrm{\mathbb{Z}Mod}\left(R\right)=\mathrm{\mathbb{Z}Mod}\left(R\right)$$
6		rrextdrg	$$⊢R\in \mathrm{ℝExt}\to R\in \mathrm{DivRing}$$
7		rrextnrg	$$⊢R\in \mathrm{ℝExt}\to R\in \mathrm{NrmRing}$$
8	5	rrextnlm	$$⊢R\in \mathrm{ℝExt}\to \mathrm{\mathbb{Z}Mod}\left(R\right)\in \mathrm{NrmMod}$$
9		rrextchr	$$⊢R\in \mathrm{ℝExt}\to \mathrm{chr}\left(R\right)=0$$
10		rrextcusp	$$⊢R\in \mathrm{ℝExt}\to R\in \mathrm{CUnifSp}$$
11	1 2	rrextust	$$⊢R\in \mathrm{ℝExt}\to \mathrm{UnifSt}\left(R\right)=\mathrm{metUnif}\left({\mathrm{dist}\left(R\right)\upharpoonright }_{\left(B\times B\right)}\right)$$
12	2 3 1 4 5 6 7 8 9 10 11	rrhf	$$⊢R\in \mathrm{ℝExt}\to \mathrm{ℝHom}\left(R\right):ℝ⟶B$$