domneq0r

Description: Right multiplication by a nonzero element does not change zeroness in a domain. Compare rrgeq0 . (Contributed by SN, 21-Jun-2025)

	Ref	Expression
Hypotheses	domneq0r.b	$⊢ B = {Base}_{R}$
	domneq0r.0	$⊢ \underset{˙}{0} = 0_{R}$
	domneq0r.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	domneq0r.x	$⊢ φ \to X \in B$
	domneq0r.y	$⊢ φ \to Y \in (B ∖ \{\underset{˙}{0}\})$
	domneq0r.r	$⊢ φ \to R \in Domn$
Assertion	domneq0r	$⊢ φ \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow X = \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		domneq0r.b	$⊢ B = {Base}_{R}$
2		domneq0r.0	$⊢ \underset{˙}{0} = 0_{R}$
3		domneq0r.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		domneq0r.x	$⊢ φ \to X \in B$
5		domneq0r.y	$⊢ φ \to Y \in (B ∖ \{\underset{˙}{0}\})$
6		domneq0r.r	$⊢ φ \to R \in Domn$
7		domnring	$⊢ R \in Domn \to R \in Ring$
8	6 7	syl	$⊢ φ \to R \in Ring$
9	5	eldifad	$⊢ φ \to Y \in B$
10	1 3 2 8 9	ringlzd	$⊢ φ \to \underset{˙}{0} \underset{˙}{\cdot} Y = \underset{˙}{0}$
11	10	eqeq2d	$⊢ φ \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \underset{˙}{\cdot} Y \leftrightarrow X \underset{˙}{\cdot} Y = \underset{˙}{0})$
12	1 2	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in B$
13	8 12	syl	$⊢ φ \to \underset{˙}{0} \in B$
14	1 2 3 4 13 5 6	domnrcanb	$⊢ φ \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \underset{˙}{\cdot} Y \leftrightarrow X = \underset{˙}{0})$
15	11 14	bitr3d	$⊢ φ \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow X = \underset{˙}{0})$

Metamath Proof Explorer