Theorem cmsms

Description: A complete metric space is a metric space. (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Assertion	cmsms	$$⊢G\in \mathrm{CMetSp}\to G\in \mathrm{MetSp}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
2		eqid	$$⊢{\mathrm{dist}\left(G\right)\upharpoonright }_{\left({\mathrm{Base}}_G\times {\mathrm{Base}}_G\right)}={\mathrm{dist}\left(G\right)\upharpoonright }_{\left({\mathrm{Base}}_G\times {\mathrm{Base}}_G\right)}$$
3	1 2	iscms	$$⊢G\in \mathrm{CMetSp}\leftrightarrow \left(G\in \mathrm{MetSp}\wedge {\mathrm{dist}\left(G\right)\upharpoonright }_{\left({\mathrm{Base}}_G\times {\mathrm{Base}}_G\right)}\in \mathrm{CMet}\left({\mathrm{Base}}_G\right)\right)$$
4	3	simplbi	$$⊢G\in \mathrm{CMetSp}\to G\in \mathrm{MetSp}$$