Theorem xmetf

Description: Mapping of the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xmetf	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D:X\times X⟶{ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to X\in \mathrm{dom}\mathrm{\infty Met}$$
2		isxmet	$$⊢X\in \mathrm{dom}\mathrm{\infty Met}\to \left(D\in \mathrm{\infty Met}\left(X\right)\leftrightarrow \left(D:X\times X⟶{ℝ}^{*}\wedge \forall x\in X\forall y\in X\left(\left(xDy=0\leftrightarrow x=y\right)\wedge \forall z\in XxDy\le \left(zDx\right){+}_{𝑒}\left(zDy\right)\right)\right)\right)$$
3	1 2	syl	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(D\in \mathrm{\infty Met}\left(X\right)\leftrightarrow \left(D:X\times X⟶{ℝ}^{*}\wedge \forall x\in X\forall y\in X\left(\left(xDy=0\leftrightarrow x=y\right)\wedge \forall z\in XxDy\le \left(zDx\right){+}_{𝑒}\left(zDy\right)\right)\right)\right)$$
4	3	ibi	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(D:X\times X⟶{ℝ}^{*}\wedge \forall x\in X\forall y\in X\left(\left(xDy=0\leftrightarrow x=y\right)\wedge \forall z\in XxDy\le \left(zDx\right){+}_{𝑒}\left(zDy\right)\right)\right)$$
5	4	simpld	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D:X\times X⟶{ℝ}^{*}$$