nrgdomn

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

		Ref	Expression
	Assertion	nrgdomn	$⊢ R \in NrmRing \to (R \in Domn \leftrightarrow R \in NzRing)$

Step	Hyp	Ref	Expression
1		domnnzr	$⊢ R \in Domn \to R \in NzRing$
2		simpr	$⊢ (R \in NrmRing \land R \in NzRing) \to R \in NzRing$
3		eqid	$⊢ norm (R) = norm (R)$
4		eqid	$⊢ AbsVal (R) = AbsVal (R)$
5	3 4	nrgabv	$⊢ R \in NrmRing \to norm (R) \in AbsVal (R)$
6	5	ne0d	$⊢ R \in NrmRing \to AbsVal (R) \neq \emptyset$
7	6	adantr	$⊢ (R \in NrmRing \land R \in NzRing) \to AbsVal (R) \neq \emptyset$
8	4	abvn0b	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land AbsVal (R) \neq \emptyset)$
9	2 7 8	sylanbrc	$⊢ (R \in NrmRing \land R \in NzRing) \to R \in Domn$
10	9	ex	$⊢ R \in NrmRing \to (R \in NzRing \to R \in Domn)$
11	1 10	impbid2	$⊢ R \in NrmRing \to (R \in Domn \leftrightarrow R \in NzRing)$

Metamath Proof Explorer