Theorem unitnz

Description: In a nonzero ring, a unit cannot be zero. (Contributed by Thierry Arnoux, 25-Apr-2025)

	Ref	Expression
Hypotheses	unitnz.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
	unitnz.2	$$⊢\underset{\dot{}}{0}=0_R$$
	unitnz.3	$$⊢\phi \to R\in \mathrm{NzRing}$$
	unitnz.4	$$⊢\phi \to X\in U$$
Assertion	unitnz	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		unitnz.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
2		unitnz.2	$$⊢\underset{\dot{}}{0}=0_R$$
3		unitnz.3	$$⊢\phi \to R\in \mathrm{NzRing}$$
4		unitnz.4	$$⊢\phi \to X\in U$$
5		nzrring	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$
6	3 5	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
7		eqid	$$⊢1_R=1_R$$
8	7 2	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne \underset{\dot{}}{0}$$
9	3 8	syl	$$⊢\phi \to 1_R\ne \underset{\dot{}}{0}$$
10	1 2 7	0unit	$$⊢R\in \mathrm{Ring}\to \left(\underset{\dot{}}{0}\in U\leftrightarrow 1_R=\underset{\dot{}}{0}\right)$$
11	10	necon3bbid	$$⊢R\in \mathrm{Ring}\to \left(\neg \underset{\dot{}}{0}\in U\leftrightarrow 1_R\ne \underset{\dot{}}{0}\right)$$
12	11	biimpar	$$⊢\left(R\in \mathrm{Ring}\wedge 1_R\ne \underset{\dot{}}{0}\right)\to \neg \underset{\dot{}}{0}\in U$$
13	6 9 12	syl2anc	$$⊢\phi \to \neg \underset{\dot{}}{0}\in U$$
14		nelne2	$$⊢\left(X\in U\wedge \neg \underset{\dot{}}{0}\in U\right)\to X\ne \underset{\dot{}}{0}$$
15	4 13 14	syl2anc	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$