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