Theorem ngpgrp 24756

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3905   ∘ ccom 5665  ‘cfv 6536  distcds 17314  Grpcgrp 18995  -_gcsg 18997  MetSpcms 24475  normcnm 24733  NrmGrpcngp 24734

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-co 5670  df-iota 6492  df-fv 6544  df-ngp 24740

This theorem is referenced by:  ngpds  24761  ngpds2  24763  ngpds3  24765  ngprcan  24767  isngp4  24769  ngpinvds  24770  ngpsubcan  24771  nmf  24772  nmge0  24774  nmeq0  24775  nminv  24778  nmmtri  24779  nmsub  24780  nmrtri  24781  nm2dif  24782  nmtri  24783  nmtri2  24784  ngpi  24785  nm0  24786  ngptgp  24793  tngngp2  24809  tnggrpr  24812  nrmtngnrm  24815  nlmdsdi  24838  nlmdsdir  24839  nrginvrcnlem  24848  ngpocelbl  24861  nmo0  24892  nmotri  24896  0nghm  24898  nmoid  24899  idnghm  24900  nmods  24901  nmcn  25002  nmoleub2lem2  25275  nmhmcn  25279  cphpyth  25375  cphipval2  25400  4cphipval2  25401  cphipval  25402  ipcnlem2  25403  nglmle  25461  qqhcn  34381