Theorem ngpgrp 23853

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

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3897   ∘ ccom 5618  ‘cfv 6473  distcds 17060  Grpcgrp 18665  -_gcsg 18667  MetSpcms 23569  normcnm 23830  NrmGrpcngp 23831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-opab 5152  df-co 5623  df-iota 6425  df-fv 6481  df-ngp 23837

This theorem is referenced by:  ngpds  23858  ngpds2  23860  ngpds3  23862  ngprcan  23864  isngp4  23866  ngpinvds  23867  ngpsubcan  23868  nmf  23869  nmge0  23871  nmeq0  23872  nminv  23875  nmmtri  23876  nmsub  23877  nmrtri  23878  nm2dif  23879  nmtri  23880  nmtri2  23881  ngpi  23882  nm0  23883  ngptgp  23890  tngngp2  23914  tnggrpr  23917  nrmtngnrm  23920  nlmdsdi  23943  nlmdsdir  23944  nrginvrcnlem  23953  ngpocelbl  23966  nmo0  23997  nmotri  24001  0nghm  24003  nmoid  24004  idnghm  24005  nmods  24006  nmcn  24105  nmoleub2lem2  24377  nmhmcn  24381  cphpyth  24478  cphipval2  24503  4cphipval2  24504  cphipval  24505  ipcnlem2  24506  nglmle  24564  qqhcn  32180