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

Theorem ngpgrp 23135
Description: A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.)
Assertion
Ref Expression
ngpgrp (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp)

Proof of Theorem ngpgrp
StepHypRef Expression
1 eqid 2818 . . 3 (norm‘𝐺) = (norm‘𝐺)
2 eqid 2818 . . 3 (-g𝐺) = (-g𝐺)
3 eqid 2818 . . 3 (dist‘𝐺) = (dist‘𝐺)
41, 2, 3isngp 23132 . 2 (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((norm‘𝐺) ∘ (-g𝐺)) ⊆ (dist‘𝐺)))
54simp1bi 1137 1 (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wss 3933  ccom 5552  cfv 6348  distcds 16562  Grpcgrp 18041  -gcsg 18043  MetSpcms 22855  normcnm 23113  NrmGrpcngp 23114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-co 5557  df-iota 6307  df-fv 6356  df-ngp 23120
This theorem is referenced by:  ngpds  23140  ngpds2  23142  ngpds3  23144  ngprcan  23146  isngp4  23148  ngpinvds  23149  ngpsubcan  23150  nmf  23151  nmge0  23153  nmeq0  23154  nminv  23157  nmmtri  23158  nmsub  23159  nmrtri  23160  nm2dif  23161  nmtri  23162  nmtri2  23163  ngpi  23164  nm0  23165  ngptgp  23172  tngngp2  23188  tnggrpr  23191  nrmtngnrm  23194  nlmdsdi  23217  nlmdsdir  23218  nrginvrcnlem  23227  ngpocelbl  23240  nmo0  23271  nmotri  23275  0nghm  23277  nmoid  23278  idnghm  23279  nmods  23280  nmcn  23379  nmoleub2lem2  23647  nmhmcn  23651  cphipval2  23771  4cphipval2  23772  cphipval  23773  ipcnlem2  23774  nglmle  23832  qqhcn  31131
  Copyright terms: Public domain W3C validator