Theorem domnmuln0rd

Description: In a domain, factors of a nonzero product are nonzero. (Contributed by Thierry Arnoux, 8-Jun-2025)

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

Proof

Step	Hyp	Ref	Expression
1		domnmuln0rd.b	$$⊢B={\mathrm{Base}}_R$$
2		domnmuln0rd.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		domnmuln0rd.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		domnmuln0rd.1	$$⊢\phi \to R\in \mathrm{Domn}$$
5		domnmuln0rd.2	$$⊢\phi \to X\in B$$
6		domnmuln0rd.3	$$⊢\phi \to Y\in B$$
7		domnmuln0rd.4	$$⊢\phi \to X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}$$
8	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)$$
9	4 5 6 8	syl3anc	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)$$
10	9	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)$$
11	7 10	mpbid	$$⊢\phi \to \neg \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)$$
12		ioran	$$⊢\neg \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\leftrightarrow \left(\neg X=\underset{\dot{}}{0}\wedge \neg Y=\underset{\dot{}}{0}\right)$$
13	11 12	sylib	$$⊢\phi \to \left(\neg X=\underset{\dot{}}{0}\wedge \neg Y=\underset{\dot{}}{0}\right)$$
14		neqne	$$⊢\neg X=\underset{\dot{}}{0}\to X\ne \underset{\dot{}}{0}$$
15		neqne	$$⊢\neg Y=\underset{\dot{}}{0}\to Y\ne \underset{\dot{}}{0}$$
16	14 15	anim12i	$$⊢\left(\neg X=\underset{\dot{}}{0}\wedge \neg Y=\underset{\dot{}}{0}\right)\to \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)$$
17	13 16	syl	$$⊢\phi \to \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)$$