Theorem rrhval

Description: Value of the canonical homormorphism from the real numbers to a complete space. (Contributed by Thierry Arnoux, 2-Nov-2017)

	Ref	Expression
Hypotheses	rrhval.1	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	rrhval.2	$$⊢K=\mathrm{TopOpen}\left(R\right)$$
Assertion	rrhval	$$⊢R\in V\to \mathrm{ℝHom}\left(R\right)=\left(J\mathrm{CnExt}K\right)\left(\mathrm{\mathbb{Q}Hom}\left(R\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrhval.1	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		rrhval.2	$$⊢K=\mathrm{TopOpen}\left(R\right)$$
3		elex	$$⊢R\in V\to R\in \mathrm{V}$$
4	1	eqcomi	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=J$$
5	4	a1i	$$⊢r=R\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=J$$
6		fveq2	$$⊢r=R\to \mathrm{TopOpen}\left(r\right)=\mathrm{TopOpen}\left(R\right)$$
7	6 2	eqtr4di	$$⊢r=R\to \mathrm{TopOpen}\left(r\right)=K$$
8	5 7	oveq12d	$$⊢r=R\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{TopOpen}\left(r\right)=J\mathrm{CnExt}K$$
9		fveq2	$$⊢r=R\to \mathrm{\mathbb{Q}Hom}\left(r\right)=\mathrm{\mathbb{Q}Hom}\left(R\right)$$
10	8 9	fveq12d	$$⊢r=R\to \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)=\left(J\mathrm{CnExt}K\right)\left(\mathrm{\mathbb{Q}Hom}\left(R\right)\right)$$
11		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)$$
12		fvex	$$⊢\left(J\mathrm{CnExt}K\right)\left(\mathrm{\mathbb{Q}Hom}\left(R\right)\right)\in \mathrm{V}$$
13	10 11 12	fvmpt	$$⊢R\in \mathrm{V}\to \mathrm{ℝHom}\left(R\right)=\left(J\mathrm{CnExt}K\right)\left(\mathrm{\mathbb{Q}Hom}\left(R\right)\right)$$
14	3 13	syl	$$⊢R\in V\to \mathrm{ℝHom}\left(R\right)=\left(J\mathrm{CnExt}K\right)\left(\mathrm{\mathbb{Q}Hom}\left(R\right)\right)$$