Theorem ngpgrp 24582

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

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3883   ∘ ccom 5622  ‘cfv 6485  distcds 17220  Grpcgrp 18900  -_gcsg 18902  MetSpcms 24301  normcnm 24559  NrmGrpcngp 24560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-co 5627  df-iota 6441  df-fv 6493  df-ngp 24566

This theorem is referenced by:  ngpds  24587  ngpds2  24589  ngpds3  24591  ngprcan  24593  isngp4  24595  ngpinvds  24596  ngpsubcan  24597  nmf  24598  nmge0  24600  nmeq0  24601  nminv  24604  nmmtri  24605  nmsub  24606  nmrtri  24607  nm2dif  24608  nmtri  24609  nmtri2  24610  ngpi  24611  nm0  24612  ngptgp  24619  tngngp2  24635  tnggrpr  24638  nrmtngnrm  24641  nlmdsdi  24664  nlmdsdir  24665  nrginvrcnlem  24674  ngpocelbl  24687  nmo0  24718  nmotri  24722  0nghm  24724  nmoid  24725  idnghm  24726  nmods  24727  nmcn  24828  nmoleub2lem2  25101  nmhmcn  25105  cphpyth  25201  cphipval2  25226  4cphipval2  25227  cphipval  25228  ipcnlem2  25229  nglmle  25287  qqhcn  34175