Theorem ngpgrp 24108

Description: A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.)

Assertion

Ref	Expression
ngpgrp	⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp)

Proof of Theorem ngpgrp

Step	Hyp	Ref	Expression
1		eqid 2733	. . 3 ⊢ (norm‘𝐺) = (norm‘𝐺)
2		eqid 2733	. . 3 ⊢ (-g‘𝐺) = (-g‘𝐺)
3		eqid 2733	. . 3 ⊢ (dist‘𝐺) = (dist‘𝐺)
4	1, 2, 3	isngp 24105	. 2 ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((norm‘𝐺) ∘ (-g‘𝐺)) ⊆ (dist‘𝐺)))
5	4	simp1bi 1146	1 ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3949   ∘ ccom 5681  ‘cfv 6544  distcds 17206  Grpcgrp 18819  -_gcsg 18821  MetSpcms 23824  normcnm 24085  NrmGrpcngp 24086

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 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-co 5686  df-iota 6496  df-fv 6552  df-ngp 24092

This theorem is referenced by:  ngpds  24113  ngpds2  24115  ngpds3  24117  ngprcan  24119  isngp4  24121  ngpinvds  24122  ngpsubcan  24123  nmf  24124  nmge0  24126  nmeq0  24127  nminv  24130  nmmtri  24131  nmsub  24132  nmrtri  24133  nm2dif  24134  nmtri  24135  nmtri2  24136  ngpi  24137  nm0  24138  ngptgp  24145  tngngp2  24169  tnggrpr  24172  nrmtngnrm  24175  nlmdsdi  24198  nlmdsdir  24199  nrginvrcnlem  24208  ngpocelbl  24221  nmo0  24252  nmotri  24256  0nghm  24258  nmoid  24259  idnghm  24260  nmods  24261  nmcn  24360  nmoleub2lem2  24632  nmhmcn  24636  cphpyth  24733  cphipval2  24758  4cphipval2  24759  cphipval  24760  ipcnlem2  24761  nglmle  24819  qqhcn  32971