Theorem isms

Description: Express the predicate " <. X , D >. is a metric space" with underlying set X and distance function D . (Contributed by NM, 27-Aug-2006) (Revised by Mario Carneiro, 24-Aug-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	isms	$$⊢K\in \mathrm{MetSp}\leftrightarrow \left(K\in \mathrm{\infty MetSp}\wedge D\in \mathrm{Met}\left(X\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{dist}\left(f\right)=\mathrm{dist}\left(K\right)$$
5		fveq2	$$⊢f=K\to {\mathrm{Base}}_f={\mathrm{Base}}_K$$
6	5 2	syl6eqr	$$⊢f=K\to {\mathrm{Base}}_f=X$$
7	6	sqxpeqd	$$⊢f=K\to {\mathrm{Base}}_f\times {\mathrm{Base}}_f=X\times X$$
8	4 7	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)}$$
9	8 3	syl6eqr	$$⊢f=K\to {\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}=D$$
10	6	fveq2d	$$⊢f=K\to \mathrm{Met}\left({\mathrm{Base}}_f\right)=\mathrm{Met}\left(X\right)$$
11	9 10	eleq12d	$$⊢f=K\to \left({\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\in \mathrm{Met}\left({\mathrm{Base}}_f\right)\leftrightarrow D\in \mathrm{Met}\left(X\right)\right)$$
12		df-ms	$$⊢\mathrm{MetSp}=\left\{f\in \mathrm{\infty MetSp}|{\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\in \mathrm{Met}\left({\mathrm{Base}}_f\right)\right\}$$
13	11 12	elrab2	$$⊢K\in \mathrm{MetSp}\leftrightarrow \left(K\in \mathrm{\infty MetSp}\wedge D\in \mathrm{Met}\left(X\right)\right)$$