Theorem idomnzd

Description: A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by AV, 12-Jul-2026)

	Ref	Expression
Hypotheses	isidom3.b	$$⊢B={\mathrm{Base}}_R$$
	isidom3.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	isidom3.0	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	idomnzd	$$⊢\left(R\in \mathrm{IDomn}\wedge \left(X\in B\wedge Y\in B\wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\right)\to \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		isidom3.b	$$⊢B={\mathrm{Base}}_R$$
2		isidom3.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		isidom3.0	$$⊢\underset{\dot{}}{0}=0_R$$
4		eqid	$$⊢1_R=1_R$$
5	1 2 3 4	isidom3	$$⊢R\in \mathrm{IDomn}\leftrightarrow \left(R\in \mathrm{CRing}\wedge \underset{\dot{}}{0}\ne 1_R\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\right)$$
6	5	simp3bi	$$⊢R\in \mathrm{IDomn}\to \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)$$
7		oveq1	$$⊢a=X\to a\underset{\dot{}}{·}b=X\underset{\dot{}}{·}b$$
8	7	eqeq1d	$$⊢a=X\to \left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\leftrightarrow X\underset{\dot{}}{·}b=\underset{\dot{}}{0}\right)$$
9		eqeq1	$$⊢a=X\to \left(a=\underset{\dot{}}{0}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
10	9	orbi1d	$$⊢a=X\to \left(\left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\leftrightarrow \left(X=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)$$
11	8 10	imbi12d	$$⊢a=X\to \left(\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(X\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(X=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\right)$$
12		oveq2	$$⊢b=Y\to X\underset{\dot{}}{·}b=X\underset{\dot{}}{·}Y$$
13	12	eqeq1d	$$⊢b=Y\to \left(X\underset{\dot{}}{·}b=\underset{\dot{}}{0}\leftrightarrow X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
14		eqeq1	$$⊢b=Y\to \left(b=\underset{\dot{}}{0}\leftrightarrow Y=\underset{\dot{}}{0}\right)$$
15	14	orbi2d	$$⊢b=Y\to \left(\left(X=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\leftrightarrow \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)$$
16	13 15	imbi12d	$$⊢b=Y\to \left(\left(X\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(X=\underset{\dot{}}{0}\vee b=\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)$$
17	11 16	rspc2v	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)\right)$$
18	6 17	syl5com	$$⊢R\in \mathrm{IDomn}\to \left(\left(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)\right)$$
19	18	expd	$$⊢R\in \mathrm{IDomn}\to \left(X\in B\to \left(Y\in B\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)\right)\right)$$
20	19	3imp2	$$⊢\left(R\in \mathrm{IDomn}\wedge \left(X\in B\wedge Y\in B\wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\right)\to \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)$$