Theorem ngpgrp 24809

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3906   ∘ ccom 5667  ‘cfv 6540  distcds 17343  Grpcgrp 19046  -_gcsg 19048  MetSpcms 24528  normcnm 24786  NrmGrpcngp 24787

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-co 5672  df-iota 6496  df-fv 6548  df-ngp 24793

This theorem is used by:  ngpds  24814  ngpds2  24816  ngpds3  24818  ngprcan  24820  isngp4  24822  ngpinvds  24823  ngpsubcan  24824  nmf  24825  nmge0  24827  nmeq0  24828  nminv  24831  nmmtri  24832  nmsub  24833  nmrtri  24834  nm2dif  24835  nmtri  24836  nmtri2  24837  ngpi  24838  nm0  24839  ngptgp  24846  tngngp2  24862  tnggrpr  24865  nrmtngnrm  24868  nlmdsdi  24891  nlmdsdir  24892  nrginvrcnlem  24901  ngpocelbl  24914  nmo0  24945  nmotri  24949  0nghm  24951  nmoid  24952  idnghm  24953  nmods  24954  nmcn  25055  nmoleub2lem2  25328  nmhmcn  25332  cphpyth  25428  cphipval2  25453  4cphipval2  25454  cphipval  25455  ipcnlem2  25456  nglmle  25514  qqhcn  34447