Theorem ngpgrp 24493

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3916   ∘ ccom 5644  ‘cfv 6513  distcds 17235  Grpcgrp 18871  -_gcsg 18873  MetSpcms 24212  normcnm 24470  NrmGrpcngp 24471

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-co 5649  df-iota 6466  df-fv 6521  df-ngp 24477

This theorem is referenced by:  ngpds  24498  ngpds2  24500  ngpds3  24502  ngprcan  24504  isngp4  24506  ngpinvds  24507  ngpsubcan  24508  nmf  24509  nmge0  24511  nmeq0  24512  nminv  24515  nmmtri  24516  nmsub  24517  nmrtri  24518  nm2dif  24519  nmtri  24520  nmtri2  24521  ngpi  24522  nm0  24523  ngptgp  24530  tngngp2  24546  tnggrpr  24549  nrmtngnrm  24552  nlmdsdi  24575  nlmdsdir  24576  nrginvrcnlem  24585  ngpocelbl  24598  nmo0  24629  nmotri  24633  0nghm  24635  nmoid  24636  idnghm  24637  nmods  24638  nmcn  24739  nmoleub2lem2  25022  nmhmcn  25026  cphpyth  25122  cphipval2  25147  4cphipval2  25148  cphipval  25149  ipcnlem2  25150  nglmle  25208  qqhcn  33987