Theorem nrgring

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

	Ref	Expression
Assertion	nrgring	⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( norm ‘ 𝑅 ) = ( norm ‘ 𝑅 )
2		eqid	⊢ ( AbsVal ‘ 𝑅 ) = ( AbsVal ‘ 𝑅 )
3	1 2	nrgabv	⊢ ( 𝑅 ∈ NrmRing → ( norm ‘ 𝑅 ) ∈ ( AbsVal ‘ 𝑅 ) )
4	2	abvrcl	⊢ ( ( norm ‘ 𝑅 ) ∈ ( AbsVal ‘ 𝑅 ) → 𝑅 ∈ Ring )
5	3 4	syl	⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ Ring )