Theorem nrgngp

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

	Ref	Expression
Assertion	nrgngp	$$⊢R\in \mathrm{NrmRing}\to R\in \mathrm{NrmGrp}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{norm}\left(R\right)=\mathrm{norm}\left(R\right)$$
2		eqid	$$⊢\mathrm{AbsVal}\left(R\right)=\mathrm{AbsVal}\left(R\right)$$
3	1 2	isnrg	$$⊢R\in \mathrm{NrmRing}\leftrightarrow \left(R\in \mathrm{NrmGrp}\wedge \mathrm{norm}\left(R\right)\in \mathrm{AbsVal}\left(R\right)\right)$$
4	3	simplbi	$$⊢R\in \mathrm{NrmRing}\to R\in \mathrm{NrmGrp}$$