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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 iscms.1 ⊢ X = Base M
2 iscms.2 ⊢ D = dist ⁡ M ↾ X × X
3 1 2 iscms ⊢ M ∈ CMetSp ↔ M ∈ MetSp ∧ D ∈ CMet ⁡ X
4 3 simprbi ⊢ M ∈ CMetSp → D ∈ CMet ⁡ X