unitnz

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

Step	Hyp	Ref	Expression
1		unitnz.1	$⊢ U = Unit (R)$
2		unitnz.2	$⊢ \underset{˙}{0} = 0_{R}$
3		unitnz.3	$⊢ φ \to R \in NzRing$
4		unitnz.4	$⊢ φ \to X \in U$
5		nzrring	$⊢ R \in NzRing \to R \in Ring$
6	3 5	syl	$⊢ φ \to R \in Ring$
7		eqid	$⊢ 1_{R} = 1_{R}$
8	7 2	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq \underset{˙}{0}$
9	3 8	syl	$⊢ φ \to 1_{R} \neq \underset{˙}{0}$
10	1 2 7	0unit	$⊢ R \in Ring \to (\underset{˙}{0} \in U \leftrightarrow 1_{R} = \underset{˙}{0})$
11	10	necon3bbid	$⊢ R \in Ring \to (\neg \underset{˙}{0} \in U \leftrightarrow 1_{R} \neq \underset{˙}{0})$
12	11	biimpar	$⊢ (R \in Ring \land 1_{R} \neq \underset{˙}{0}) \to \neg \underset{˙}{0} \in U$
13	6 9 12	syl2anc	$⊢ φ \to \neg \underset{˙}{0} \in U$
14		nelne2	$⊢ (X \in U \land \neg \underset{˙}{0} \in U) \to X \neq \underset{˙}{0}$
15	4 13 14	syl2anc	$⊢ φ \to X \neq \underset{˙}{0}$

Metamath Proof Explorer