Theorem ngpms 24768

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142   ⊆ wss 3904   ∘ ccom 5664  ‘cfv 6536  distcds 17325  Grpcgrp 19006  -_gcsg 19008  MetSpcms 24486  normcnm 24744  NrmGrpcngp 24745

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-co 5669  df-iota 6492  df-fv 6544  df-ngp 24751

This theorem is used by:  ngpxms  24769  ngptps  24770  ngpmet  24771  isngp4  24780  nmmtri  24790  nmrtri  24792  subgngp  24803  ngptgp  24804  tngngp2  24820  nlmvscnlem2  24853  nlmvscnlem1  24854  nlmvscn  24855  nrginvrcn  24860  nghmcn  24913  nmcn  25013  nmhmcn  25290  ipcnlem2  25414  ipcnlem1  25415  ipcn  25416  nglmle  25472  cssbn  25545  minveclem2  25596  minveclem3b  25598  minveclem3  25599  minveclem4  25602  minveclem7  25605