Theorem nrgngp 24724

Description: A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)

Assertion

Ref	Expression
nrgngp	⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)

Proof of Theorem nrgngp

Step	Hyp	Ref	Expression
1		eqid 2764	. . 3 ⊢ (norm‘𝑅) = (norm‘𝑅)
2		eqid 2764	. . 3 ⊢ (AbsVal‘𝑅) = (AbsVal‘𝑅)
3	1, 2	isnrg 24722	. 2 ⊢ (𝑅 ∈ NrmRing ↔ (𝑅 ∈ NrmGrp ∧ (norm‘𝑅) ∈ (AbsVal‘𝑅)))
4	3	simplbi 500	1 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)

Syntax hints:   → wi 4   ∈ wcel 2144  ‘cfv 6523  AbsValcabv 20859  normcnm 24638  NrmGrpcngp 24639  NrmRingcnrg 24641

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-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-iota 6479  df-fv 6531  df-nrg 24647

This theorem is referenced by:  nrgdsdi  24727  nrgdsdir  24728  unitnmn0  24730  nminvr  24731  nmdvr  24732  nrgtgp  24734  subrgnrg  24735  nlmngp2  24742  sranlm  24746  nrginvrcnlem  24753  nrginvrcn  24754  cnzh  34267  rezh  34268  qqhcn  34290  qqhucn  34291  rrhcn  34296  rrhf  34297  rrexttps  34305  rrexthaus  34306