Theorem ngpgrp 24826

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899   ∘ ccom 5659  ‘cfv 6533  distcds 17352  Grpcgrp 19058  -_gcsg 19060  MetSpcms 24545  normcnm 24803  NrmGrpcngp 24804

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-co 5664  df-iota 6489  df-fv 6541  df-ngp 24810

This theorem is used by:  ngpds  24831  ngpds2  24833  ngpds3  24835  ngprcan  24837  isngp4  24839  ngpinvds  24840  ngpsubcan  24841  nmf  24842  nmge0  24844  nmeq0  24845  nminv  24848  nmmtri  24849  nmsub  24850  nmrtri  24851  nm2dif  24852  nmtri  24853  nmtri2  24854  ngpi  24855  nm0  24856  ngptgp  24863  tngngp2  24879  tnggrpr  24882  nrmtngnrm  24885  nlmdsdi  24908  nlmdsdir  24909  nrginvrcnlem  24918  ngpocelbl  24931  nmo0  24962  nmotri  24966  0nghm  24968  nmoid  24969  idnghm  24970  nmods  24971  nmcn  25072  nmoleub2lem2  25345  nmhmcn  25349  cphpyth  25445  cphipval2  25470  4cphipval2  25471  cphipval  25472  ipcnlem2  25473  nglmle  25531  qqhcn  34502