Theorem ngpgrp 24659

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

Syntax hints:   → wi 4   ∈ wcel 2142   ⊆ wss 3904   ∘ ccom 5651  ‘cfv 6521  distcds 17295  Grpcgrp 18975  -_gcsg 18977  MetSpcms 24378  normcnm 24636  NrmGrpcngp 24637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-co 5656  df-iota 6477  df-fv 6529  df-ngp 24643

This theorem is referenced by:  ngpds  24664  ngpds2  24666  ngpds3  24668  ngprcan  24670  isngp4  24672  ngpinvds  24673  ngpsubcan  24674  nmf  24675  nmge0  24677  nmeq0  24678  nminv  24681  nmmtri  24682  nmsub  24683  nmrtri  24684  nm2dif  24685  nmtri  24686  nmtri2  24687  ngpi  24688  nm0  24689  ngptgp  24696  tngngp2  24712  tnggrpr  24715  nrmtngnrm  24718  nlmdsdi  24741  nlmdsdir  24742  nrginvrcnlem  24751  ngpocelbl  24764  nmo0  24795  nmotri  24799  0nghm  24801  nmoid  24802  idnghm  24803  nmods  24804  nmcn  24905  nmoleub2lem2  25178  nmhmcn  25182  cphpyth  25278  cphipval2  25303  4cphipval2  25304  cphipval  25305  ipcnlem2  25306  nglmle  25364  qqhcn  34288