ringunitnzdiv

Description: In a unitary ring, a unit 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$
	ringunitnzdiv.x	$⊢ φ \to X \in Unit (R)$
Assertion	ringunitnzdiv	$⊢ φ \to (X \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		ringunitnzdiv.x	$⊢ φ \to X \in Unit (R)$
7		eqid	$⊢ 1_{R} = 1_{R}$
8		eqid	$⊢ Unit (R) = Unit (R)$
9	1 8	unitcl	$⊢ X \in Unit (R) \to X \in B$
10	6 9	syl	$⊢ φ \to X \in B$
11		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
12	8 11 1	ringinvcl	$⊢ (R \in Ring \land X \in Unit (R)) \to {inv}_{r} (R) (X) \in B$
13	4 6 12	syl2anc	$⊢ φ \to {inv}_{r} (R) (X) \in B$
14		oveq1	$⊢ e = {inv}_{r} (R) (X) \to e \underset{˙}{\cdot} X = {inv}_{r} (R) (X) \underset{˙}{\cdot} X$
15	14	eqeq1d	$⊢ e = {inv}_{r} (R) (X) \to (e \underset{˙}{\cdot} X = 1_{R} \leftrightarrow {inv}_{r} (R) (X) \underset{˙}{\cdot} X = 1_{R})$
16	15	adantl	$⊢ (φ \land e = {inv}_{r} (R) (X)) \to (e \underset{˙}{\cdot} X = 1_{R} \leftrightarrow {inv}_{r} (R) (X) \underset{˙}{\cdot} X = 1_{R})$
17	8 11 3 7	unitlinv	$⊢ (R \in Ring \land X \in Unit (R)) \to {inv}_{r} (R) (X) \underset{˙}{\cdot} X = 1_{R}$
18	4 6 17	syl2anc	$⊢ φ \to {inv}_{r} (R) (X) \underset{˙}{\cdot} X = 1_{R}$
19	13 16 18	rspcedvd	$⊢ φ \to \exists e \in B e \underset{˙}{\cdot} X = 1_{R}$
20	1 3 7 2 4 10 19 5	ringinvnzdiv	$⊢ φ \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow Y = \underset{˙}{0})$

Metamath Proof Explorer