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={\mathrm{Base}}_R$$
	drngmuleq0.o	$$⊢\underset{\dot{}}{0}=0_R$$
	drngmuleq0.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	drngmuleq0.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
	drngmuleq0.x	$$⊢\phi \to X\in B$$
	drngmuleq0.y	$$⊢\phi \to Y\in B$$
Assertion	drngmulne0	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}\leftrightarrow \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		drngmuleq0.b	$$⊢B={\mathrm{Base}}_R$$
2		drngmuleq0.o	$$⊢\underset{\dot{}}{0}=0_R$$
3		drngmuleq0.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		drngmuleq0.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
5		drngmuleq0.x	$$⊢\phi \to X\in B$$
6		drngmuleq0.y	$$⊢\phi \to Y\in B$$
7	1 2 3 4 5 6	drngmul0or	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)$$
8	7	necon3abid	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}\leftrightarrow \neg \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)$$
9		neanior	$$⊢\left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\leftrightarrow \neg \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)$$
10	8 9	bitr4di	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}\leftrightarrow \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)$$