Theorem tmsxms

Description: The constructed metric space is an extended metric space. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypothesis	tmsbas.k	$$⊢K=\mathrm{toMetSp}\left(D\right)$$
Assertion	tmsxms	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to K\in \mathrm{\infty MetSp}$$

Proof

Step	Hyp	Ref	Expression
1		tmsbas.k	$$⊢K=\mathrm{toMetSp}\left(D\right)$$
2	1	tmsds	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D=\mathrm{dist}\left(K\right)$$
3	1	tmsbas	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to X={\mathrm{Base}}_K$$
4	3	fveq2d	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{\infty Met}\left(X\right)=\mathrm{\infty Met}\left({\mathrm{Base}}_K\right)$$
5	2 4	eleq12d	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(D\in \mathrm{\infty Met}\left(X\right)\leftrightarrow \mathrm{dist}\left(K\right)\in \mathrm{\infty Met}\left({\mathrm{Base}}_K\right)\right)$$
6	5	ibi	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{dist}\left(K\right)\in \mathrm{\infty Met}\left({\mathrm{Base}}_K\right)$$
7		ssid	$$⊢{\mathrm{Base}}_K\subseteq {\mathrm{Base}}_K$$
8		xmetres2	$$⊢\left(\mathrm{dist}\left(K\right)\in \mathrm{\infty Met}\left({\mathrm{Base}}_K\right)\wedge {\mathrm{Base}}_K\subseteq {\mathrm{Base}}_K\right)\to {\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\in \mathrm{\infty Met}\left({\mathrm{Base}}_K\right)$$
9	6 7 8	sylancl	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to {\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\in \mathrm{\infty Met}\left({\mathrm{Base}}_K\right)$$
10		xmetf	$$⊢\mathrm{dist}\left(K\right)\in \mathrm{\infty Met}\left({\mathrm{Base}}_K\right)\to \mathrm{dist}\left(K\right):{\mathrm{Base}}_K\times {\mathrm{Base}}_K⟶{ℝ}^{*}$$
11		ffn	$$⊢\mathrm{dist}\left(K\right):{\mathrm{Base}}_K\times {\mathrm{Base}}_K⟶{ℝ}^{*}\to \mathrm{dist}\left(K\right)Fn\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)$$
12		fnresdm	$$⊢\mathrm{dist}\left(K\right)Fn\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)\to {\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}=\mathrm{dist}\left(K\right)$$
13	6 10 11 12	4syl	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to {\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}=\mathrm{dist}\left(K\right)$$
14	13 2	eqtr4d	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to {\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}=D$$
15	14	fveq2d	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{MetOpen}\left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\right)=\mathrm{MetOpen}\left(D\right)$$
16		eqid	$$⊢\mathrm{MetOpen}\left(D\right)=\mathrm{MetOpen}\left(D\right)$$
17	1 16	tmstopn	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{MetOpen}\left(D\right)=\mathrm{TopOpen}\left(K\right)$$
18	15 17	eqtr2d	$$⊢D\in \mathrm{\infty Met}\left(X\right)\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)$$
19		eqid	$$⊢\mathrm{TopOpen}\left(K\right)=\mathrm{TopOpen}\left(K\right)$$
20		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
21		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)}$$
22	19 20 21	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)$$
23	9 18 22	sylanbrc	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to K\in \mathrm{\infty MetSp}$$