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 = ( Base ` R )
	domneq0r.0	|- .0. = ( 0g ` R )
	domneq0r.m	|- .x. = ( .r ` R )
	domneq0r.x	|- ( ph -> X e. B )
	domneq0r.y	|- ( ph -> Y e. ( B \ { .0. } ) )
	domneq0r.r	|- ( ph -> R e. Domn )
Assertion	domneq0r	|- ( ph -> ( ( X .x. Y ) = .0. <-> X = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		domneq0r.b	|- B = ( Base ` R )
2		domneq0r.0	|- .0. = ( 0g ` R )
3		domneq0r.m	|- .x. = ( .r ` R )
4		domneq0r.x	|- ( ph -> X e. B )
5		domneq0r.y	|- ( ph -> Y e. ( B \ { .0. } ) )
6		domneq0r.r	|- ( ph -> R e. Domn )
7		domnring	|- ( R e. Domn -> R e. Ring )
8	6 7	syl	|- ( ph -> R e. Ring )
9	5	eldifad	|- ( ph -> Y e. B )
10	1 3 2 8 9	ringlzd	|- ( ph -> ( .0. .x. Y ) = .0. )
11	10	eqeq2d	|- ( ph -> ( ( X .x. Y ) = ( .0. .x. Y ) <-> ( X .x. Y ) = .0. ) )
12	1 2	ring0cl	|- ( R e. Ring -> .0. e. B )
13	8 12	syl	|- ( ph -> .0. e. B )
14	1 2 3 4 13 5 6	domnrcanb	|- ( ph -> ( ( X .x. Y ) = ( .0. .x. Y ) <-> X = .0. ) )
15	11 14	bitr3d	|- ( ph -> ( ( X .x. Y ) = .0. <-> X = .0. ) )