Metamath Proof Explorer


Theorem drngmulne0

Description: A product is nonzero iff both its factors are nonzero. (Contributed by NM, 18-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 )
Assertion drngmulne0
|- ( ph -> ( ( X .x. Y ) =/= .0. <-> ( X =/= .0. /\ Y =/= .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 1 2 3 4 5 6 drngmul0or
 |-  ( ph -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )
8 7 necon3abid
 |-  ( ph -> ( ( X .x. Y ) =/= .0. <-> -. ( X = .0. \/ Y = .0. ) ) )
9 neanior
 |-  ( ( X =/= .0. /\ Y =/= .0. ) <-> -. ( X = .0. \/ Y = .0. ) )
10 8 9 bitr4di
 |-  ( ph -> ( ( X .x. Y ) =/= .0. <-> ( X =/= .0. /\ Y =/= .0. ) ) )