MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ngpms Structured version   Visualization version   GIF version

Theorem ngpms 23979
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
StepHypRef Expression
1 eqid 2733 . . 3 (normβ€˜πΊ) = (normβ€˜πΊ)
2 eqid 2733 . . 3 (-gβ€˜πΊ) = (-gβ€˜πΊ)
3 eqid 2733 . . 3 (distβ€˜πΊ) = (distβ€˜πΊ)
41, 2, 3isngp 23975 . 2 (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((normβ€˜πΊ) ∘ (-gβ€˜πΊ)) βŠ† (distβ€˜πΊ)))
54simp2bi 1147 1 (𝐺 ∈ NrmGrp β†’ 𝐺 ∈ MetSp)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∈ wcel 2107   βŠ† wss 3914   ∘ ccom 5641  β€˜cfv 6500  distcds 17150  Grpcgrp 18756  -gcsg 18758  MetSpcms 23694  normcnm 23955  NrmGrpcngp 23956
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-co 5646  df-iota 6452  df-fv 6508  df-ngp 23962
This theorem is referenced by:  ngpxms  23980  ngptps  23981  ngpmet  23982  isngp4  23991  nmmtri  24001  nmrtri  24003  subgngp  24014  ngptgp  24015  tngngp2  24039  nlmvscnlem2  24072  nlmvscnlem1  24073  nlmvscn  24074  nrginvrcn  24079  nghmcn  24132  nmcn  24230  nmhmcn  24506  ipcnlem2  24631  ipcnlem1  24632  ipcn  24633  nglmle  24689  cssbn  24762  minveclem2  24813  minveclem3b  24815  minveclem3  24816  minveclem4  24819  minveclem7  24822
  Copyright terms: Public domain W3C validator