Theorem nrgngp 24583

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6499  AbsValcabv 20728  normcnm 24497  NrmGrpcngp 24498  NrmRingcnrg 24500

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-nrg 24506

This theorem is referenced by:  nrgdsdi  24586  nrgdsdir  24587  unitnmn0  24589  nminvr  24590  nmdvr  24591  nrgtgp  24593  subrgnrg  24594  nlmngp2  24601  sranlm  24605  nrginvrcnlem  24612  nrginvrcn  24613  cnzh  33951  rezh  33952  qqhcn  33974  qqhucn  33975  rrhcn  33980  rrhf  33981  rrexttps  33989  rrexthaus  33990