Theorem isdomn6

Description: A ring is a domain iff nonzero-divisors are all the nonzero elements. (Contributed by Thierry Arnoux, 6-May-2025)

	Ref	Expression
Hypotheses	isdomn6.b	$$⊢B={\mathrm{Base}}_R$$
	isdomn6.t	$$⊢E=\mathrm{RLReg}\left(R\right)$$
	isdomn6.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	isdomn6	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge B\setminus \left\{\underset{\dot{}}{0}\right\}=E\right)$$

Proof

Step	Hyp	Ref	Expression
1		isdomn6.b	$$⊢B={\mathrm{Base}}_R$$
2		isdomn6.t	$$⊢E=\mathrm{RLReg}\left(R\right)$$
3		isdomn6.z	$$⊢\underset{\dot{}}{0}=0_R$$
4	1 2 3	isdomn2	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq E\right)$$
5	2 1	rrgss	$$⊢E\subseteq B$$
6	5	a1i	$$⊢R\in \mathrm{NzRing}\to E\subseteq B$$
7	2 3	rrgnz	$$⊢R\in \mathrm{NzRing}\to \neg \underset{\dot{}}{0}\in E$$
8		ssdifsn	$$⊢E\subseteq B\setminus \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \left(E\subseteq B\wedge \neg \underset{\dot{}}{0}\in E\right)$$
9	6 7 8	sylanbrc	$$⊢R\in \mathrm{NzRing}\to E\subseteq B\setminus \left\{\underset{\dot{}}{0}\right\}$$
10		sssseq	$$⊢E\subseteq B\setminus \left\{\underset{\dot{}}{0}\right\}\to \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq E\leftrightarrow B\setminus \left\{\underset{\dot{}}{0}\right\}=E\right)$$
11	9 10	syl	$$⊢R\in \mathrm{NzRing}\to \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq E\leftrightarrow B\setminus \left\{\underset{\dot{}}{0}\right\}=E\right)$$
12	11	pm5.32i	$$⊢\left(R\in \mathrm{NzRing}\wedge B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq E\right)\leftrightarrow \left(R\in \mathrm{NzRing}\wedge B\setminus \left\{\underset{\dot{}}{0}\right\}=E\right)$$
13	4 12	bitri	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge B\setminus \left\{\underset{\dot{}}{0}\right\}=E\right)$$