Theorem ngpgrp 24494

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3917   ∘ ccom 5645  ‘cfv 6514  distcds 17236  Grpcgrp 18872  -_gcsg 18874  MetSpcms 24213  normcnm 24471  NrmGrpcngp 24472

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 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-co 5650  df-iota 6467  df-fv 6522  df-ngp 24478

This theorem is referenced by:  ngpds  24499  ngpds2  24501  ngpds3  24503  ngprcan  24505  isngp4  24507  ngpinvds  24508  ngpsubcan  24509  nmf  24510  nmge0  24512  nmeq0  24513  nminv  24516  nmmtri  24517  nmsub  24518  nmrtri  24519  nm2dif  24520  nmtri  24521  nmtri2  24522  ngpi  24523  nm0  24524  ngptgp  24531  tngngp2  24547  tnggrpr  24550  nrmtngnrm  24553  nlmdsdi  24576  nlmdsdir  24577  nrginvrcnlem  24586  ngpocelbl  24599  nmo0  24630  nmotri  24634  0nghm  24636  nmoid  24637  idnghm  24638  nmods  24639  nmcn  24740  nmoleub2lem2  25023  nmhmcn  25027  cphpyth  25123  cphipval2  25148  4cphipval2  25149  cphipval  25150  ipcnlem2  25151  nglmle  25209  qqhcn  33988