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

Metamath Proof Explorer

Theorem drngmuleq0

Description: An element is zero iff its product with a nonzero element is zero. (Contributed by NM, 8-Oct-2014)

Ref Expression
Hypotheses drngmuleq0.b 
|- B = ( Base ` R )
drngmuleq0.o 
|- .0. = ( 0g ` R )
drngmuleq0.t 
|- .x. = ( .r ` R )
drngmuleq0.r 
|- ( ph -> R e. DivRing )
drngmuleq0.x 
|- ( ph -> X e. B )
drngmuleq0.y 
|- ( ph -> Y e. B )
drngmuleq0.e 
|- ( ph -> Y =/= .0. )
Assertion drngmuleq0 
|- ( ph -> ( ( X .x. Y ) = .0. <-> X = .0. ) )

Proof

Step Hyp Ref Expression
1 drngmuleq0.b 
 |-  B = ( Base ` R )
2 drngmuleq0.o 
 |-  .0. = ( 0g ` R )
3 drngmuleq0.t 
 |-  .x. = ( .r ` R )
4 drngmuleq0.r 
 |-  ( ph -> R e. DivRing )
5 drngmuleq0.x 
 |-  ( ph -> X e. B )
6 drngmuleq0.y 
 |-  ( ph -> Y e. B )
7 drngmuleq0.e 
 |-  ( ph -> Y =/= .0. )
8 1 2 3 4 5 6 drngmul0or 
 |-  ( ph -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )
9 df-ne 
 |-  ( Y =/= .0. <-> -. Y = .0. )
10 orel2 
 |-  ( -. Y = .0. -> ( ( X = .0. \/ Y = .0. ) -> X = .0. ) )
11 orc 
 |-  ( X = .0. -> ( X = .0. \/ Y = .0. ) )
12 10 11 impbid1 
 |-  ( -. Y = .0. -> ( ( X = .0. \/ Y = .0. ) <-> X = .0. ) )
13 9 12 sylbi 
 |-  ( Y =/= .0. -> ( ( X = .0. \/ Y = .0. ) <-> X = .0. ) )
14 7 13 syl 
 |-  ( ph -> ( ( X = .0. \/ Y = .0. ) <-> X = .0. ) )
15 8 14 bitrd 
 |-  ( ph -> ( ( X .x. Y ) = .0. <-> X = .0. ) )