Theorem cmscmet

Description: The induced metric on a complete normed group is complete. (Contributed 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	cmscmet	$$⊢M\in \mathrm{CMetSp}\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	1 2	iscms	$$⊢M\in \mathrm{CMetSp}\leftrightarrow \left(M\in \mathrm{MetSp}\wedge D\in \mathrm{CMet}\left(X\right)\right)$$
4	3	simprbi	$$⊢M\in \mathrm{CMetSp}\to D\in \mathrm{CMet}\left(X\right)$$