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

Theorem ngpgrp 23978
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 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β€˜πΊ)))
54simp1bi 1146 1 (𝐺 ∈ NrmGrp β†’ 𝐺 ∈ Grp)
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:  ngpds  23983  ngpds2  23985  ngpds3  23987  ngprcan  23989  isngp4  23991  ngpinvds  23992  ngpsubcan  23993  nmf  23994  nmge0  23996  nmeq0  23997  nminv  24000  nmmtri  24001  nmsub  24002  nmrtri  24003  nm2dif  24004  nmtri  24005  nmtri2  24006  ngpi  24007  nm0  24008  ngptgp  24015  tngngp2  24039  tnggrpr  24042  nrmtngnrm  24045  nlmdsdi  24068  nlmdsdir  24069  nrginvrcnlem  24078  ngpocelbl  24091  nmo0  24122  nmotri  24126  0nghm  24128  nmoid  24129  idnghm  24130  nmods  24131  nmcn  24230  nmoleub2lem2  24502  nmhmcn  24506  cphpyth  24603  cphipval2  24628  4cphipval2  24629  cphipval  24630  ipcnlem2  24631  nglmle  24689  qqhcn  32636
  Copyright terms: Public domain W3C validator