Metamath Proof Explorer

Theorem isnrg

Description: A normed ring is a ring with a norm that makes it into a normed group, and such that the norm is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015)

		Ref	Expression
	Hypotheses	isnrg.1	$⊢ N = norm (R)$
		isnrg.2	$⊢ A = AbsVal (R)$
	Assertion	isnrg	$⊢ R \in NrmRing \leftrightarrow (R \in NrmGrp \land N \in A)$

Proof

Step	Hyp	Ref	Expression
1		isnrg.1	$⊢ N = norm (R)$
2		isnrg.2	$⊢ A = AbsVal (R)$
3		fveq2	$⊢ r = R \to norm (r) = norm (R)$
4	3 1	eqtr4di	$⊢ r = R \to norm (r) = N$
5		fveq2	$⊢ r = R \to AbsVal (r) = AbsVal (R)$
6	5 2	eqtr4di	$⊢ r = R \to AbsVal (r) = A$
7	4 6	eleq12d	$⊢ r = R \to (norm (r) \in AbsVal (r) \leftrightarrow N \in A)$
8		df-nrg	$⊢ NrmRing = \{r \in NrmGrp \| norm (r) \in AbsVal (r)\}$
9	7 8	elrab2	$⊢ R \in NrmRing \leftrightarrow (R \in NrmGrp \land N \in A)$