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 = ( Base ` M )
	iscms.2	|- D = ( ( dist ` M ) |` ( X X. X ) )
Assertion	cmscmet	|- ( M e. CMetSp -> D e. ( CMet ` X ) )

Proof

Step	Hyp	Ref	Expression
1		iscms.1	|- X = ( Base ` M )
2		iscms.2	|- D = ( ( dist ` M ) |` ( X X. X ) )
3	1 2	iscms	|- ( M e. CMetSp <-> ( M e. MetSp /\ D e. ( CMet ` X ) ) )
4	3	simprbi	|- ( M e. CMetSp -> D e. ( CMet ` X ) )