Theorem setsxms

Description: The constructed metric space is a metric space iff the provided distance function is a metric. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypotheses	setsms.x	$$⊢\phi \to X={\mathrm{Base}}_M$$
	setsms.d	$$⊢\phi \to D={\mathrm{dist}\left(M\right)\upharpoonright }_{\left(X\times X\right)}$$
	setsms.k	$$⊢\phi \to K=M\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(D\right)⟩$$
	setsms.m	$$⊢\phi \to M\in V$$
Assertion	setsxms	$$⊢\phi \to \left(K\in \mathrm{\infty MetSp}\leftrightarrow D\in \mathrm{\infty Met}\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		setsms.x	$$⊢\phi \to X={\mathrm{Base}}_M$$
2		setsms.d	$$⊢\phi \to D={\mathrm{dist}\left(M\right)\upharpoonright }_{\left(X\times X\right)}$$
3		setsms.k	$$⊢\phi \to K=M\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(D\right)⟩$$
4		setsms.m	$$⊢\phi \to M\in V$$
5	1 2 3 4	setsmstopn	$$⊢\phi \to \mathrm{MetOpen}\left(D\right)=\mathrm{TopOpen}\left(K\right)$$
6	1 2 3	setsmsds	$$⊢\phi \to \mathrm{dist}\left(M\right)=\mathrm{dist}\left(K\right)$$
7	1 2 3	setsmsbas	$$⊢\phi \to X={\mathrm{Base}}_K$$
8	7	sqxpeqd	$$⊢\phi \to X\times X={\mathrm{Base}}_K\times {\mathrm{Base}}_K$$
9	6 8	reseq12d	$$⊢\phi \to {\mathrm{dist}\left(M\right)\upharpoonright }_{\left(X\times X\right)}={\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}$$
10	2 9	eqtrd	$$⊢\phi \to D={\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}$$
11	10	fveq2d	$$⊢\phi \to \mathrm{MetOpen}\left(D\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\right)$$
12	5 11	eqtr3d	$$⊢\phi \to \mathrm{TopOpen}\left(K\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\right)$$
13		eqid	$$⊢\mathrm{TopOpen}\left(K\right)=\mathrm{TopOpen}\left(K\right)$$
14		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
15		eqid	$$⊢{\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}={\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}$$
16	13 14 15	isxms2	$$⊢K\in \mathrm{\infty MetSp}\leftrightarrow \left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\in \mathrm{\infty Met}\left({\mathrm{Base}}_K\right)\wedge \mathrm{TopOpen}\left(K\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\right)\right)$$
17	16	rbaib	$$⊢\mathrm{TopOpen}\left(K\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\right)\to \left(K\in \mathrm{\infty MetSp}\leftrightarrow {\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\in \mathrm{\infty Met}\left({\mathrm{Base}}_K\right)\right)$$
18	12 17	syl	$$⊢\phi \to \left(K\in \mathrm{\infty MetSp}\leftrightarrow {\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\in \mathrm{\infty Met}\left({\mathrm{Base}}_K\right)\right)$$
19	7	fveq2d	$$⊢\phi \to \mathrm{\infty Met}\left(X\right)=\mathrm{\infty Met}\left({\mathrm{Base}}_K\right)$$
20	10 19	eleq12d	$$⊢\phi \to \left(D\in \mathrm{\infty Met}\left(X\right)\leftrightarrow {\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\in \mathrm{\infty Met}\left({\mathrm{Base}}_K\right)\right)$$
21	18 20	bitr4d	$$⊢\phi \to \left(K\in \mathrm{\infty MetSp}\leftrightarrow D\in \mathrm{\infty Met}\left(X\right)\right)$$