Theorem ngpgrp 24543

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 24540	. 2 ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((norm‘𝐺) ∘ (-g‘𝐺)) ⊆ (dist‘𝐺)))
5	4	simp1bi 1145	1 ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3901   ∘ ccom 5628  ‘cfv 6492  distcds 17186  Grpcgrp 18863  -_gcsg 18865  MetSpcms 24262  normcnm 24520  NrmGrpcngp 24521

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-co 5633  df-iota 6448  df-fv 6500  df-ngp 24527

This theorem is referenced by:  ngpds  24548  ngpds2  24550  ngpds3  24552  ngprcan  24554  isngp4  24556  ngpinvds  24557  ngpsubcan  24558  nmf  24559  nmge0  24561  nmeq0  24562  nminv  24565  nmmtri  24566  nmsub  24567  nmrtri  24568  nm2dif  24569  nmtri  24570  nmtri2  24571  ngpi  24572  nm0  24573  ngptgp  24580  tngngp2  24596  tnggrpr  24599  nrmtngnrm  24602  nlmdsdi  24625  nlmdsdir  24626  nrginvrcnlem  24635  ngpocelbl  24648  nmo0  24679  nmotri  24683  0nghm  24685  nmoid  24686  idnghm  24687  nmods  24688  nmcn  24789  nmoleub2lem2  25072  nmhmcn  25076  cphpyth  25172  cphipval2  25197  4cphipval2  25198  cphipval  25199  ipcnlem2  25200  nglmle  25258  qqhcn  34148