Theorem bncmet

Description: The induced metric on Banach space is complete. (Contributed by NM, 8-Sep-2007) (Revised by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypotheses	iscms.1	$$⊢X={\mathrm{Base}}_M$$
	iscms.2	$$⊢D={\mathrm{dist}\left(M\right)\upharpoonright }_{\left(X\times X\right)}$$
Assertion	bncmet	$$⊢M\in \mathrm{Ban}\to D\in \mathrm{CMet}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		iscms.1	$$⊢X={\mathrm{Base}}_M$$
2		iscms.2	$$⊢D={\mathrm{dist}\left(M\right)\upharpoonright }_{\left(X\times X\right)}$$
3		bncms	$$⊢M\in \mathrm{Ban}\to M\in \mathrm{CMetSp}$$
4	1 2	cmscmet	$$⊢M\in \mathrm{CMetSp}\to D\in \mathrm{CMet}\left(X\right)$$
5	3 4	syl	$$⊢M\in \mathrm{Ban}\to D\in \mathrm{CMet}\left(X\right)$$