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	⊢ 𝑋 = ( Base ‘ 𝑀 )
	iscms.2	⊢ 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) )
Assertion	bncmet	⊢ ( 𝑀 ∈ Ban → 𝐷 ∈ ( CMet ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		iscms.1	⊢ 𝑋 = ( Base ‘ 𝑀 )
2		iscms.2	⊢ 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) )
3		bncms	⊢ ( 𝑀 ∈ Ban → 𝑀 ∈ CMetSp )
4	1 2	cmscmet	⊢ ( 𝑀 ∈ CMetSp → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
5	3 4	syl	⊢ ( 𝑀 ∈ Ban → 𝐷 ∈ ( CMet ‘ 𝑋 ) )