Theorem ngpms 24946

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900   ∘ ccom 5659  ‘cfv 6555  distcds 17463  Grpcgrp 19170  -_gcsg 19172  MetSpcms 24664  normcnm 24922  NrmGrpcngp 24923

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-co 5664  df-iota 6509  df-fv 6563  df-ngp 24929

This theorem is used by:  ngpxms  24947  ngptps  24948  ngpmet  24949  isngp4  24958  nmmtri  24968  nmrtri  24970  subgngp  24981  ngptgp  24982  tngngp2  24998  nlmvscnlem2  25031  nlmvscnlem1  25032  nlmvscn  25033  nrginvrcn  25038  nghmcn  25091  nmcn  25191  nmhmcn  25468  ipcnlem2  25592  ipcnlem1  25593  ipcn  25594  nglmle  25650  cssbn  25723  minveclem2  25774  minveclem3b  25776  minveclem3  25777  minveclem4  25780  minveclem7  25783