Theorem isdomn2

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

	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		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$$
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	8	imbi2d	$$⊢x\in B\to \left(\left(x\ne \underset{\dot{}}{0}\to x\in E\right)\leftrightarrow \left(x\ne \underset{\dot{}}{0}\to \forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)\right)$$
10	9	ralbiia	$$⊢\forall x\in B\left(x\ne \underset{\dot{}}{0}\to x\in E\right)\leftrightarrow \forall x\in B\left(x\ne \underset{\dot{}}{0}\to \forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
11		eldifsn	$$⊢x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)$$
12	11	imbi1i	$$⊢\left(x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to x\in E\right)\leftrightarrow \left(\left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\to x\in E\right)$$
13		impexp	$$⊢\left(\left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\to x\in E\right)\leftrightarrow \left(x\in B\to \left(x\ne \underset{\dot{}}{0}\to x\in E\right)\right)$$
14	12 13	bitri	$$⊢\left(x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to x\in E\right)\leftrightarrow \left(x\in B\to \left(x\ne \underset{\dot{}}{0}\to x\in E\right)\right)$$
15	14	ralbii2	$$⊢\forall x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)x\in E\leftrightarrow \forall x\in B\left(x\ne \underset{\dot{}}{0}\to x\in E\right)$$
16		con34b	$$⊢\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(\neg \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\to \neg x{\cdot }_{R}y=\underset{\dot{}}{0}\right)$$
17		impexp	$$⊢\left(\left(\neg x=\underset{\dot{}}{0}\wedge \neg y=\underset{\dot{}}{0}\right)\to \neg x{\cdot }_{R}y=\underset{\dot{}}{0}\right)\leftrightarrow \left(\neg x=\underset{\dot{}}{0}\to \left(\neg y=\underset{\dot{}}{0}\to \neg x{\cdot }_{R}y=\underset{\dot{}}{0}\right)\right)$$
18		ioran	$$⊢\neg \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\leftrightarrow \left(\neg x=\underset{\dot{}}{0}\wedge \neg y=\underset{\dot{}}{0}\right)$$
19	18	imbi1i	$$⊢\left(\neg \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\to \neg x{\cdot }_{R}y=\underset{\dot{}}{0}\right)\leftrightarrow \left(\left(\neg x=\underset{\dot{}}{0}\wedge \neg y=\underset{\dot{}}{0}\right)\to \neg x{\cdot }_{R}y=\underset{\dot{}}{0}\right)$$
20		df-ne	$$⊢x\ne \underset{\dot{}}{0}\leftrightarrow \neg x=\underset{\dot{}}{0}$$
21		con34b	$$⊢\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\leftrightarrow \left(\neg y=\underset{\dot{}}{0}\to \neg x{\cdot }_{R}y=\underset{\dot{}}{0}\right)$$
22	20 21	imbi12i	$$⊢\left(x\ne \underset{\dot{}}{0}\to \left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(\neg x=\underset{\dot{}}{0}\to \left(\neg y=\underset{\dot{}}{0}\to \neg x{\cdot }_{R}y=\underset{\dot{}}{0}\right)\right)$$
23	17 19 22	3bitr4i	$$⊢\left(\neg \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\to \neg x{\cdot }_{R}y=\underset{\dot{}}{0}\right)\leftrightarrow \left(x\ne \underset{\dot{}}{0}\to \left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
24	16 23	bitri	$$⊢\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(x\ne \underset{\dot{}}{0}\to \left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
25	24	ralbii	$$⊢\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 y\in B\left(x\ne \underset{\dot{}}{0}\to \left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
26		r19.21v	$$⊢\forall y\in B\left(x\ne \underset{\dot{}}{0}\to \left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(x\ne \underset{\dot{}}{0}\to \forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
27	25 26	bitri	$$⊢\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 \left(x\ne \underset{\dot{}}{0}\to \forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
28	27	ralbii	$$⊢\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 B\left(x\ne \underset{\dot{}}{0}\to \forall y\in B\left(x{\cdot }_{R}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
29	10 15 28	3bitr4i	$$⊢\forall x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)x\in E\leftrightarrow \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)$$
30	6 29	bitr2i	$$⊢\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$$
31	30	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)$$
32	5 31	bitri	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq E\right)$$