Theorem domneq0

Description: In a domain, a product is zero iff it has a zero factor. (Contributed by Mario Carneiro, 28-Mar-2015)

	Ref	Expression
Hypotheses	domneq0.b	$$⊢B={\mathrm{Base}}_R$$
	domneq0.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	domneq0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	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)$$

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		3simpc	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge Y\in B\right)\to \left(X\in B\wedge Y\in B\right)$$
5	1 2 3	isdomn	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\right)$$
6	5	simprbi	$$⊢R\in \mathrm{Domn}\to \forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)$$
7	6	3ad2ant1	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge Y\in B\right)\to \forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)$$
8		oveq1	$$⊢x=X\to x\underset{\dot{}}{·}y=X\underset{\dot{}}{·}y$$
9	8	eqeq1d	$$⊢x=X\to \left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\leftrightarrow X\underset{\dot{}}{·}y=\underset{\dot{}}{0}\right)$$
10		eqeq1	$$⊢x=X\to \left(x=\underset{\dot{}}{0}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
11	10	orbi1d	$$⊢x=X\to \left(\left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\leftrightarrow \left(X=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)$$
12	9 11	imbi12d	$$⊢x=X\to \left(\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(X\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(X=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\right)$$
13		oveq2	$$⊢y=Y\to X\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y$$
14	13	eqeq1d	$$⊢y=Y\to \left(X\underset{\dot{}}{·}y=\underset{\dot{}}{0}\leftrightarrow X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
15		eqeq1	$$⊢y=Y\to \left(y=\underset{\dot{}}{0}\leftrightarrow Y=\underset{\dot{}}{0}\right)$$
16	15	orbi2d	$$⊢y=Y\to \left(\left(X=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\leftrightarrow \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)$$
17	14 16	imbi12d	$$⊢y=Y\to \left(\left(X\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(X=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)\right)$$
18	12 17	rspc2va	$$⊢\left(\left(X\in B\wedge Y\in B\right)\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\right)\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)$$
19	4 7 18	syl2anc	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)$$
20		domnring	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{Ring}$$
21	20	3ad2ant1	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge Y\in B\right)\to R\in \mathrm{Ring}$$
22		simp3	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge Y\in B\right)\to Y\in B$$
23	1 2 3	ringlz	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}Y=\underset{\dot{}}{0}$$
24	21 22 23	syl2anc	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge Y\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}Y=\underset{\dot{}}{0}$$
25		oveq1	$$⊢X=\underset{\dot{}}{0}\to X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\underset{\dot{}}{·}Y$$
26	25	eqeq1d	$$⊢X=\underset{\dot{}}{0}\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
27	24 26	syl5ibrcom	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge Y\in B\right)\to \left(X=\underset{\dot{}}{0}\to X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
28		simp2	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge Y\in B\right)\to X\in B$$
29	1 2 3	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
30	21 28 29	syl2anc	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
31		oveq2	$$⊢Y=\underset{\dot{}}{0}\to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}\underset{\dot{}}{0}$$
32	31	eqeq1d	$$⊢Y=\underset{\dot{}}{0}\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)$$
33	30 32	syl5ibrcom	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge Y\in B\right)\to \left(Y=\underset{\dot{}}{0}\to X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
34	27 33	jaod	$$⊢\left(R\in \mathrm{Domn}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\to X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
35	19 34	impbid	$$⊢\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)$$