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 = ( norm ` R )
	isnrg.2	|- A = ( AbsVal ` R )
Assertion	nrgabv	|- ( R e. NrmRing -> N e. A )

Proof

Step	Hyp	Ref	Expression
1		isnrg.1	|- N = ( norm ` R )
2		isnrg.2	|- A = ( AbsVal ` R )
3	1 2	isnrg	|- ( R e. NrmRing <-> ( R e. NrmGrp /\ N e. A ) )
4	3	simprbi	|- ( R e. NrmRing -> N e. A )