Theorem ngpms 24662

Description: A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)

Assertion

Ref	Expression
ngpms	⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp)

Proof of Theorem ngpms

Step	Hyp	Ref	Expression
1		eqid 2764	. . 3 ⊢ (norm‘𝐺) = (norm‘𝐺)
2		eqid 2764	. . 3 ⊢ (-g‘𝐺) = (-g‘𝐺)
3		eqid 2764	. . 3 ⊢ (dist‘𝐺) = (dist‘𝐺)
4	1, 2, 3	isngp 24658	. 2 ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((norm‘𝐺) ∘ (-g‘𝐺)) ⊆ (dist‘𝐺)))
5	4	simp2bi 1160	1 ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp)

Syntax hints:   → wi 4   ∈ wcel 2144   ⊆ wss 3906   ∘ ccom 5653  ‘cfv 6523  distcds 17297  Grpcgrp 18977  -_gcsg 18979  MetSpcms 24380  normcnm 24638  NrmGrpcngp 24639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-co 5658  df-iota 6479  df-fv 6531  df-ngp 24645

This theorem is referenced by:  ngpxms  24663  ngptps  24664  ngpmet  24665  isngp4  24674  nmmtri  24684  nmrtri  24686  subgngp  24697  ngptgp  24698  tngngp2  24714  nlmvscnlem2  24747  nlmvscnlem1  24748  nlmvscn  24749  nrginvrcn  24754  nghmcn  24807  nmcn  24907  nmhmcn  25184  ipcnlem2  25308  ipcnlem1  25309  ipcn  25310  nglmle  25366  cssbn  25439  minveclem2  25490  minveclem3b  25492  minveclem3  25493  minveclem4  25496  minveclem7  25499