This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nrgring

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

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

Step	Hyp	Ref	Expression
1		eqid	$⊢ norm (R) = norm (R)$
2		eqid	$⊢ AbsVal (R) = AbsVal (R)$
3	1 2	nrgabv	$⊢ R \in NrmRing \to norm (R) \in AbsVal (R)$
4	2	abvrcl	$⊢ norm (R) \in AbsVal (R) \to R \in Ring$
5	3 4	syl	$⊢ R \in NrmRing \to R \in Ring$