Theorem domnrrg

Description: In a domain, any nonzero element is a nonzero-divisor. (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	domnrrg	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to X\in E$$

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	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	4	simprbi	$$⊢R\in \mathrm{Domn}\to B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq E$$
6	5	3ad2ant1	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq E$$
7		simp2	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to X\in B$$
8		simp3	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to X\ne \underset{\dot{}}{0}$$
9		eldifsn	$$⊢X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(X\in B\wedge X\ne \underset{\dot{}}{0}\right)$$
10	7 8 9	sylanbrc	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11	6 10	sseldd	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to X\in E$$