Theorem nrgngp 24601

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 2735	. . 3 ⊢ (norm‘𝑅) = (norm‘𝑅)
2		eqid 2735	. . 3 ⊢ (AbsVal‘𝑅) = (AbsVal‘𝑅)
3	1, 2	isnrg 24599	. 2 ⊢ (𝑅 ∈ NrmRing ↔ (𝑅 ∈ NrmGrp ∧ (norm‘𝑅) ∈ (AbsVal‘𝑅)))
4	3	simplbi 497	1 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6531  AbsValcabv 20768  normcnm 24515  NrmGrpcngp 24516  NrmRingcnrg 24518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-nrg 24524

This theorem is referenced by:  nrgdsdi  24604  nrgdsdir  24605  unitnmn0  24607  nminvr  24608  nmdvr  24609  nrgtgp  24611  subrgnrg  24612  nlmngp2  24619  sranlm  24623  nrginvrcnlem  24630  nrginvrcn  24631  cnzh  33999  rezh  34000  qqhcn  34022  qqhucn  34023  rrhcn  34028  rrhf  34029  rrexttps  34037  rrexthaus  34038