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 = ( Base ` M )
	iscms.2	|- D = ( ( dist ` M ) |` ( X X. X ) )
Assertion	bncmet	|- ( M e. Ban -> 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		bncms	|- ( M e. Ban -> M e. CMetSp )
4	1 2	cmscmet	|- ( M e. CMetSp -> D e. ( CMet ` X ) )
5	3 4	syl	|- ( M e. Ban -> D e. ( CMet ` X ) )