Definition df-rrh

Description: Define the canonical homomorphism from the real numbers to any complete field, as the extension by continuity of the canonical homomorphism from the rational numbers. (Contributed by Mario Carneiro, 22-Oct-2017) (Revised by Thierry Arnoux, 23-Oct-2017)

	Ref	Expression
Assertion	df-rrh	$$⊢\mathrm{ℝHom}=\left(r\in \mathrm{V}⟼\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{TopOpen}\left(r\right)\right)\left(\mathrm{\mathbb{Q}Hom}\left(r\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrh	$$class\mathrm{ℝHom}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		ctg	$$class\mathrm{topGen}$$
4		cioo	$$class\left(.\right)$$
5	4	crn	$$class\mathrm{ran}\left(.\right)$$
6	5 3	cfv	$$class\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
7		ccnext	$$class\mathrm{CnExt}$$
8		ctopn	$$class\mathrm{TopOpen}$$
9	1	cv	$$setvarr$$
10	9 8	cfv	$$class\mathrm{TopOpen}\left(r\right)$$
11	6 10 7	co	$$class\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{TopOpen}\left(r\right)\right)$$
12		cqqh	$$class\mathrm{\mathbb{Q}Hom}$$
13	9 12	cfv	$$class\mathrm{\mathbb{Q}Hom}\left(r\right)$$
14	13 11	cfv	$$class\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{TopOpen}\left(r\right)\right)\left(\mathrm{\mathbb{Q}Hom}\left(r\right)\right)$$
15	1 2 14	cmpt	$$class\left(r\in \mathrm{V}⟼\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{TopOpen}\left(r\right)\right)\left(\mathrm{\mathbb{Q}Hom}\left(r\right)\right)\right)$$
16	0 15	wceq	$$wff\mathrm{ℝHom}=\left(r\in \mathrm{V}⟼\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{TopOpen}\left(r\right)\right)\left(\mathrm{\mathbb{Q}Hom}\left(r\right)\right)\right)$$