This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. ) )