Theorem nrgngp 24557

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6514  AbsValcabv 20724  normcnm 24471  NrmGrpcngp 24472  NrmRingcnrg 24474

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-nrg 24480

This theorem is referenced by:  nrgdsdi  24560  nrgdsdir  24561  unitnmn0  24563  nminvr  24564  nmdvr  24565  nrgtgp  24567  subrgnrg  24568  nlmngp2  24575  sranlm  24579  nrginvrcnlem  24586  nrginvrcn  24587  cnzh  33965  rezh  33966  qqhcn  33988  qqhucn  33989  rrhcn  33994  rrhf  33995  rrexttps  34003  rrexthaus  34004