Theorem domnmuln0

Description: In a domain, a product of nonzero elements is nonzero. (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	domneq0.b	$$⊢B={\mathrm{Base}}_R$$
	domneq0.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	domneq0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	domnmuln0	$$⊢\left(R\in \mathrm{Domn}\wedge \left(X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge \left(Y\in B\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		domneq0.b	$$⊢B={\mathrm{Base}}_R$$
2		domneq0.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		domneq0.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		an4	$$⊢\left(\left(X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge \left(Y\in B\wedge Y\ne \underset{\dot{}}{0}\right)\right)\leftrightarrow \left(\left(X\in B\wedge Y\in B\right)\wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)$$
5		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)$$
6	1 2 3	domneq0	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)$$
7	6	3expb	$$⊢\left(R\in \mathrm{Domn}\wedge \left(X\in B\wedge Y\in B\right)\right)\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	$$⊢\left(R\in \mathrm{Domn}\wedge \left(X\in B\wedge Y\in B\right)\right)\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	5 8	bitr4id	$$⊢\left(R\in \mathrm{Domn}\wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(\left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\leftrightarrow X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}\right)$$
10	9	biimpd	$$⊢\left(R\in \mathrm{Domn}\wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(\left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\to X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}\right)$$
11	10	expimpd	$$⊢R\in \mathrm{Domn}\to \left(\left(\left(X\in B\wedge Y\in B\right)\wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}\right)$$
12	4 11	syl5bi	$$⊢R\in \mathrm{Domn}\to \left(\left(\left(X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge \left(Y\in B\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}\right)$$
13	12	3impib	$$⊢\left(R\in \mathrm{Domn}\wedge \left(X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge \left(Y\in B\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}$$