Theorem ngpms 24736

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 2761	. . 3 ⊢ (norm‘𝐺) = (norm‘𝐺)
2		eqid 2761	. . 3 ⊢ (-g‘𝐺) = (-g‘𝐺)
3		eqid 2761	. . 3 ⊢ (dist‘𝐺) = (dist‘𝐺)
4	1, 2, 3	isngp 24732	. 2 ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((norm‘𝐺) ∘ (-g‘𝐺)) ⊆ (dist‘𝐺)))
5	4	simp2bi 1162	1 ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp)

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3904   ∘ ccom 5665  ‘cfv 6536  distcds 17318  Grpcgrp 18999  -_gcsg 19001  MetSpcms 24454  normcnm 24712  NrmGrpcngp 24713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-co 5670  df-iota 6492  df-fv 6544  df-ngp 24719

This theorem is referenced by:  ngpxms  24737  ngptps  24738  ngpmet  24739  isngp4  24748  nmmtri  24758  nmrtri  24760  subgngp  24771  ngptgp  24772  tngngp2  24788  nlmvscnlem2  24821  nlmvscnlem1  24822  nlmvscn  24823  nrginvrcn  24828  nghmcn  24881  nmcn  24981  nmhmcn  25258  ipcnlem2  25382  ipcnlem1  25383  ipcn  25384  nglmle  25440  cssbn  25513  minveclem2  25564  minveclem3b  25566  minveclem3  25567  minveclem4  25570  minveclem7  25573