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	$⊢ \underset{˙}{0} = 0_{R}$
	drngmuleq0.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	drngmuleq0.r	$⊢ φ \to R \in DivRing$
	drngmuleq0.x	$⊢ φ \to X \in B$
	drngmuleq0.y	$⊢ φ \to Y \in B$
	drngmuleq0.e	$⊢ φ \to Y \neq \underset{˙}{0}$
Assertion	drngmuleq0	$⊢ φ \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow X = \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		drngmuleq0.b	$⊢ B = {Base}_{R}$
2		drngmuleq0.o	$⊢ \underset{˙}{0} = 0_{R}$
3		drngmuleq0.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		drngmuleq0.r	$⊢ φ \to R \in DivRing$
5		drngmuleq0.x	$⊢ φ \to X \in B$
6		drngmuleq0.y	$⊢ φ \to Y \in B$
7		drngmuleq0.e	$⊢ φ \to Y \neq \underset{˙}{0}$
8	1 2 3 4 5 6	drngmul0or	$⊢ φ \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow (X = \underset{˙}{0} \lor Y = \underset{˙}{0}))$
9		df-ne	$⊢ Y \neq \underset{˙}{0} \leftrightarrow \neg Y = \underset{˙}{0}$
10		orel2	$⊢ \neg Y = \underset{˙}{0} \to ((X = \underset{˙}{0} \lor Y = \underset{˙}{0}) \to X = \underset{˙}{0})$
11		orc	$⊢ X = \underset{˙}{0} \to (X = \underset{˙}{0} \lor Y = \underset{˙}{0})$
12	10 11	impbid1	$⊢ \neg Y = \underset{˙}{0} \to ((X = \underset{˙}{0} \lor Y = \underset{˙}{0}) \leftrightarrow X = \underset{˙}{0})$
13	9 12	sylbi	$⊢ Y \neq \underset{˙}{0} \to ((X = \underset{˙}{0} \lor Y = \underset{˙}{0}) \leftrightarrow X = \underset{˙}{0})$
14	7 13	syl	$⊢ φ \to ((X = \underset{˙}{0} \lor Y = \underset{˙}{0}) \leftrightarrow X = \underset{˙}{0})$
15	8 14	bitrd	$⊢ φ \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow X = \underset{˙}{0})$

Metamath Proof Explorer