Theorem isxms

Description: Express the predicate " <. X , D >. is an extended metric space" with underlying set X and distance function D . (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	isms.j	$$⊢J=\mathrm{TopOpen}\left(K\right)$$
	isms.x	$$⊢X={\mathrm{Base}}_K$$
	isms.d	$$⊢D={\mathrm{dist}\left(K\right)\upharpoonright }_{\left(X\times X\right)}$$
Assertion	isxms	$$⊢K\in \mathrm{\infty MetSp}\leftrightarrow \left(K\in \mathrm{TopSp}\wedge J=\mathrm{MetOpen}\left(D\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isms.j	$$⊢J=\mathrm{TopOpen}\left(K\right)$$
2		isms.x	$$⊢X={\mathrm{Base}}_K$$
3		isms.d	$$⊢D={\mathrm{dist}\left(K\right)\upharpoonright }_{\left(X\times X\right)}$$
4		fveq2	$$⊢f=K\to \mathrm{TopOpen}\left(f\right)=\mathrm{TopOpen}\left(K\right)$$
5	4 1	eqtr4di	$$⊢f=K\to \mathrm{TopOpen}\left(f\right)=J$$
6		fveq2	$$⊢f=K\to \mathrm{dist}\left(f\right)=\mathrm{dist}\left(K\right)$$
7		fveq2	$$⊢f=K\to {\mathrm{Base}}_f={\mathrm{Base}}_K$$
8	7 2	eqtr4di	$$⊢f=K\to {\mathrm{Base}}_f=X$$
9	8	sqxpeqd	$$⊢f=K\to {\mathrm{Base}}_f\times {\mathrm{Base}}_f=X\times X$$
10	6 9	reseq12d	$$⊢f=K\to {\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}={\mathrm{dist}\left(K\right)\upharpoonright }_{\left(X\times X\right)}$$
11	10 3	eqtr4di	$$⊢f=K\to {\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}=D$$
12	11	fveq2d	$$⊢f=K\to \mathrm{MetOpen}\left({\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\right)=\mathrm{MetOpen}\left(D\right)$$
13	5 12	eqeq12d	$$⊢f=K\to \left(\mathrm{TopOpen}\left(f\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\right)\leftrightarrow J=\mathrm{MetOpen}\left(D\right)\right)$$
14		df-xms	$$⊢\mathrm{\infty MetSp}=\left\{f\in \mathrm{TopSp}|\mathrm{TopOpen}\left(f\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\right)\right\}$$
15	13 14	elrab2	$$⊢K\in \mathrm{\infty MetSp}\leftrightarrow \left(K\in \mathrm{TopSp}\wedge J=\mathrm{MetOpen}\left(D\right)\right)$$