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

Proof

Step	Hyp	Ref	Expression
1		iscms.1	⊢ 𝑋 = ( Base ‘ 𝑀 )
2		iscms.2	⊢ 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) )
3	1 2	iscms	⊢ ( 𝑀 ∈ CMetSp ↔ ( 𝑀 ∈ MetSp ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )
4	3	simprbi	⊢ ( 𝑀 ∈ CMetSp → 𝐷 ∈ ( CMet ‘ 𝑋 ) )