This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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
Assertion bncmet ⊢ M ∈ Ban → D ∈ CMet ⁡ X

Proof

Step Hyp Ref Expression
1 iscms.1 ⊢ X = Base M
2 iscms.2 ⊢ D = dist ⁡ M ↾ X × X
3 bncms ⊢ M ∈ Ban → M ∈ CMetSp
4 1 2 cmscmet ⊢ M ∈ CMetSp → D ∈ CMet ⁡ X
5 3 4 syl ⊢ M ∈ Ban → D ∈ CMet ⁡ X