Theorem rrgnz

Description: In a nonzero ring, the zero is a left zero divisor (that is, not a left-regular element). (Contributed by Thierry Arnoux, 6-May-2025)

	Ref	Expression
Hypotheses	rrgnz.t	$$⊢E=\mathrm{RLReg}\left(R\right)$$
	rrgnz.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	rrgnz	$$⊢R\in \mathrm{NzRing}\to \neg \underset{\dot{}}{0}\in E$$

Proof

Step	Hyp	Ref	Expression
1		rrgnz.t	$$⊢E=\mathrm{RLReg}\left(R\right)$$
2		rrgnz.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		eqid	$$⊢1_R=1_R$$
4	3 2	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne \underset{\dot{}}{0}$$
5	4	neneqd	$$⊢R\in \mathrm{NzRing}\to \neg 1_R=\underset{\dot{}}{0}$$
6		nzrring	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$
7	6	adantr	$$⊢\left(R\in \mathrm{NzRing}\wedge \underset{\dot{}}{0}\in E\right)\to R\in \mathrm{Ring}$$
8		simpr	$$⊢\left(R\in \mathrm{NzRing}\wedge \underset{\dot{}}{0}\in E\right)\to \underset{\dot{}}{0}\in E$$
9		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
10	9 3	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
11	7 10	syl	$$⊢\left(R\in \mathrm{NzRing}\wedge \underset{\dot{}}{0}\in E\right)\to 1_R\in {\mathrm{Base}}_R$$
12		eqid	$$⊢{\cdot }_R={\cdot }_R$$
13	9 12 2 7 11	ringlzd	$$⊢\left(R\in \mathrm{NzRing}\wedge \underset{\dot{}}{0}\in E\right)\to \underset{\dot{}}{0}{\cdot }_R{1}_R=\underset{\dot{}}{0}$$
14	1 9 12 2	rrgeq0	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}\in E\wedge 1_R\in {\mathrm{Base}}_R\right)\to \left(\underset{\dot{}}{0}{\cdot }_R{1}_R=\underset{\dot{}}{0}\leftrightarrow 1_R=\underset{\dot{}}{0}\right)$$
15	14	biimpa	$$⊢\left(\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}\in E\wedge 1_R\in {\mathrm{Base}}_R\right)\wedge \underset{\dot{}}{0}{\cdot }_R{1}_R=\underset{\dot{}}{0}\right)\to 1_R=\underset{\dot{}}{0}$$
16	7 8 11 13 15	syl31anc	$$⊢\left(R\in \mathrm{NzRing}\wedge \underset{\dot{}}{0}\in E\right)\to 1_R=\underset{\dot{}}{0}$$
17	5 16	mtand	$$⊢R\in \mathrm{NzRing}\to \neg \underset{\dot{}}{0}\in E$$