Theorem 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={\mathrm{Base}}_R$$
	domneq0r.0	$$⊢\underset{\dot{}}{0}=0_R$$
	domneq0r.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	domneq0r.x	$$⊢\phi \to X\in B$$
	domneq0r.y	$$⊢\phi \to Y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	domneq0r.r	$$⊢\phi \to R\in \mathrm{Domn}$$
Assertion	domneq0r	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow X=\underset{\dot{}}{0}\right)$$

Proof

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