Theorem nrgabv

Description: The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	isnrg.1	$$⊢N=\mathrm{norm}\left(R\right)$$
	isnrg.2	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
Assertion	nrgabv	$$⊢R\in \mathrm{NrmRing}\to N\in A$$

Proof

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