Theorem nrgring

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

	Ref	Expression
Assertion	nrgring	$$⊢R\in \mathrm{NrmRing}\to R\in \mathrm{Ring}$$

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	nrgabv	$$⊢R\in \mathrm{NrmRing}\to \mathrm{norm}\left(R\right)\in \mathrm{AbsVal}\left(R\right)$$
4	2	abvrcl	$$⊢\mathrm{norm}\left(R\right)\in \mathrm{AbsVal}\left(R\right)\to R\in \mathrm{Ring}$$
5	3 4	syl	$$⊢R\in \mathrm{NrmRing}\to R\in \mathrm{Ring}$$