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