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	⊢ 𝑁 = ( norm ‘ 𝑅 )
	isnrg.2	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
Assertion	nrgabv	⊢ ( 𝑅 ∈ NrmRing → 𝑁 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		isnrg.1	⊢ 𝑁 = ( norm ‘ 𝑅 )
2		isnrg.2	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
3	1 2	isnrg	⊢ ( 𝑅 ∈ NrmRing ↔ ( 𝑅 ∈ NrmGrp ∧ 𝑁 ∈ 𝐴 ) )
4	3	simprbi	⊢ ( 𝑅 ∈ NrmRing → 𝑁 ∈ 𝐴 )