ring1nzdiv

Description: In a unitary ring, the ring unity is not a zero divisor. (Contributed by AV, 7-Mar-2025)

	Ref	Expression
Hypotheses	ringunitnzdiv.b	$⊢ B = {Base}_{R}$
	ringunitnzdiv.z	$⊢ \underset{˙}{0} = 0_{R}$
	ringunitnzdiv.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ringunitnzdiv.r	$⊢ φ \to R \in Ring$
	ringunitnzdiv.y	$⊢ φ \to Y \in B$
	ring1nzdiv.x	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	ring1nzdiv	$⊢ φ \to (\underset{˙}{1} \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow Y = \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		ringunitnzdiv.b	$⊢ B = {Base}_{R}$
2		ringunitnzdiv.z	$⊢ \underset{˙}{0} = 0_{R}$
3		ringunitnzdiv.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		ringunitnzdiv.r	$⊢ φ \to R \in Ring$
5		ringunitnzdiv.y	$⊢ φ \to Y \in B$
6		ring1nzdiv.x	$⊢ \underset{˙}{1} = 1_{R}$
7		eqid	$⊢ Unit (R) = Unit (R)$
8	7 6	1unit	$⊢ R \in Ring \to \underset{˙}{1} \in Unit (R)$
9	4 8	syl	$⊢ φ \to \underset{˙}{1} \in Unit (R)$
10	1 2 3 4 5 9	ringunitnzdiv	$⊢ φ \to (\underset{˙}{1} \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow Y = \underset{˙}{0})$

Metamath Proof Explorer