Theorem ngpms 24486

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

Assertion

Ref	Expression
ngpms	⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp)

Proof of Theorem ngpms

Step	Hyp	Ref	Expression
1		eqid 2729	. . 3 ⊢ (norm‘𝐺) = (norm‘𝐺)
2		eqid 2729	. . 3 ⊢ (-g‘𝐺) = (-g‘𝐺)
3		eqid 2729	. . 3 ⊢ (dist‘𝐺) = (dist‘𝐺)
4	1, 2, 3	isngp 24482	. 2 ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((norm‘𝐺) ∘ (-g‘𝐺)) ⊆ (dist‘𝐺)))
5	4	simp2bi 1146	1 ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp)

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3903   ∘ ccom 5623  ‘cfv 6482  distcds 17170  Grpcgrp 18812  -_gcsg 18814  MetSpcms 24204  normcnm 24462  NrmGrpcngp 24463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-co 5628  df-iota 6438  df-fv 6490  df-ngp 24469

This theorem is referenced by:  ngpxms  24487  ngptps  24488  ngpmet  24489  isngp4  24498  nmmtri  24508  nmrtri  24510  subgngp  24521  ngptgp  24522  tngngp2  24538  nlmvscnlem2  24571  nlmvscnlem1  24572  nlmvscn  24573  nrginvrcn  24578  nghmcn  24631  nmcn  24731  nmhmcn  25018  ipcnlem2  25142  ipcnlem1  25143  ipcn  25144  nglmle  25200  cssbn  25273  minveclem2  25324  minveclem3b  25326  minveclem3  25327  minveclem4  25330  minveclem7  25333