Theorem isdomn2

Description: A ring is a domain iff all nonzero elements are regular elements. (Contributed by Mario Carneiro, 28-Mar-2015) (Proof shortened by SN, 21-Jun-2025)

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

Proof

Step	Hyp	Ref	Expression
1		isdomn2.b	$$⊢B={\mathrm{Base}}_R$$
2		isdomn2.t	$$⊢E=\mathrm{RLReg}\left(R\right)$$
3		isdomn2.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		eqid	$$⊢{\cdot }_R={\cdot }_R$$
5	1 4 3	isdomn	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge \forall x\in B\forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\right)$$
6		eldifi	$$⊢x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to x\in B$$
7	2 1 4 3	isrrg	$$⊢x\in E\leftrightarrow \left(x\in B\wedge \forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
8	7	baib	$$⊢x\in B\to \left(x\in E\leftrightarrow \forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
9	6 8	syl	$$⊢x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to \left(x\in E\leftrightarrow \forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
10	9	ralbiia	$$⊢\forall x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)x\in E\leftrightarrow \forall x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)$$
11		dfss3	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq E\leftrightarrow \forall x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)x\in E$$
12		isdomn5	$$⊢\forall x\in B\forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\leftrightarrow \forall x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)$$
13	10 11 12	3bitr4ri	$$⊢\forall x\in B\forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\leftrightarrow B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq E$$
14	13	anbi2i	$$⊢\left(R\in \mathrm{NzRing}\wedge \forall x\in B\forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\right)\leftrightarrow \left(R\in \mathrm{NzRing}\wedge B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq E\right)$$
15	5 14	bitri	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq E\right)$$