Theorem domnnzr

Description: A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015)

	Ref	Expression
Assertion	domnnzr	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{NzRing}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
2		eqid	$$⊢{\cdot }_R={\cdot }_R$$
3		eqid	$$⊢0_R=0_R$$
4	1 2 3	isdomn	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\left(x{\cdot }_{R}y=0_R\to \left(x=0_R\vee y=0_R\right)\right)\right)$$
5	4	simplbi	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{NzRing}$$