Theorem ngptps

Description: A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Assertion	ngptps	⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ TopSp )

Proof

Step	Hyp	Ref	Expression
1		ngpms	⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp )
2		mstps	⊢ ( 𝐺 ∈ MetSp → 𝐺 ∈ TopSp )
3	1 2	syl	⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ TopSp )