Theorem ngpgrp 24485

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3903   ∘ ccom 5623  ‘cfv 6482  distcds 17170  Grpcgrp 18812  -_gcsg 18814  MetSpcms 24204  normcnm 24462  NrmGrpcngp 24463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-co 5628  df-iota 6438  df-fv 6490  df-ngp 24469

This theorem is referenced by:  ngpds  24490  ngpds2  24492  ngpds3  24494  ngprcan  24496  isngp4  24498  ngpinvds  24499  ngpsubcan  24500  nmf  24501  nmge0  24503  nmeq0  24504  nminv  24507  nmmtri  24508  nmsub  24509  nmrtri  24510  nm2dif  24511  nmtri  24512  nmtri2  24513  ngpi  24514  nm0  24515  ngptgp  24522  tngngp2  24538  tnggrpr  24541  nrmtngnrm  24544  nlmdsdi  24567  nlmdsdir  24568  nrginvrcnlem  24577  ngpocelbl  24590  nmo0  24621  nmotri  24625  0nghm  24627  nmoid  24628  idnghm  24629  nmods  24630  nmcn  24731  nmoleub2lem2  25014  nmhmcn  25018  cphpyth  25114  cphipval2  25139  4cphipval2  25140  cphipval  25141  ipcnlem2  25142  nglmle  25200  qqhcn  33958