Theorem drnglidl1ne0

Description: In a nonzero ring, the zero ideal is different from the unit ideal. (Contributed by Thierry Arnoux, 16-Mar-2025)

	Ref	Expression
Hypotheses	drnglidl1ne0.1	$$⊢\underset{\dot{}}{0}=0_R$$
	drnglidl1ne0.2	$$⊢B={\mathrm{Base}}_R$$
Assertion	drnglidl1ne0	$$⊢R\in \mathrm{NzRing}\to B\ne \left\{\underset{\dot{}}{0}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		drnglidl1ne0.1	$$⊢\underset{\dot{}}{0}=0_R$$
2		drnglidl1ne0.2	$$⊢B={\mathrm{Base}}_R$$
3		nzrring	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$
4		eqid	$$⊢1_R=1_R$$
5	2 4	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in B$$
6	3 5	syl	$$⊢R\in \mathrm{NzRing}\to 1_R\in B$$
7	4 1	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne \underset{\dot{}}{0}$$
8		nelsn	$$⊢1_R\ne \underset{\dot{}}{0}\to \neg 1_R\in \left\{\underset{\dot{}}{0}\right\}$$
9	7 8	syl	$$⊢R\in \mathrm{NzRing}\to \neg 1_R\in \left\{\underset{\dot{}}{0}\right\}$$
10		nelne1	$$⊢\left(1_R\in B\wedge \neg 1_R\in \left\{\underset{\dot{}}{0}\right\}\right)\to B\ne \left\{\underset{\dot{}}{0}\right\}$$
11	6 9 10	syl2anc	$$⊢R\in \mathrm{NzRing}\to B\ne \left\{\underset{\dot{}}{0}\right\}$$