Theorem ngpgrp 24555

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903   ∘ ccom 5636  ‘cfv 6500  distcds 17198  Grpcgrp 18875  -_gcsg 18877  MetSpcms 24274  normcnm 24532  NrmGrpcngp 24533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-co 5641  df-iota 6456  df-fv 6508  df-ngp 24539

This theorem is referenced by:  ngpds  24560  ngpds2  24562  ngpds3  24564  ngprcan  24566  isngp4  24568  ngpinvds  24569  ngpsubcan  24570  nmf  24571  nmge0  24573  nmeq0  24574  nminv  24577  nmmtri  24578  nmsub  24579  nmrtri  24580  nm2dif  24581  nmtri  24582  nmtri2  24583  ngpi  24584  nm0  24585  ngptgp  24592  tngngp2  24608  tnggrpr  24611  nrmtngnrm  24614  nlmdsdi  24637  nlmdsdir  24638  nrginvrcnlem  24647  ngpocelbl  24660  nmo0  24691  nmotri  24695  0nghm  24697  nmoid  24698  idnghm  24699  nmods  24700  nmcn  24801  nmoleub2lem2  25084  nmhmcn  25088  cphpyth  25184  cphipval2  25209  4cphipval2  25210  cphipval  25211  ipcnlem2  25212  nglmle  25270  qqhcn  34169