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 = {Base}_{R}$
	domnmuln0rd.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	domnmuln0rd.z	$⊢ \underset{˙}{0} = 0_{R}$
	domnmuln0rd.1	$⊢ φ \to R \in Domn$
	domnmuln0rd.2	$⊢ φ \to X \in B$
	domnmuln0rd.3	$⊢ φ \to Y \in B$
	domnmuln0rd.4	$⊢ φ \to X \underset{˙}{\cdot} Y \neq \underset{˙}{0}$
Assertion	domnmuln0rd	$⊢ φ \to (X \neq \underset{˙}{0} \land Y \neq \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		domnmuln0rd.b	$⊢ B = {Base}_{R}$
2		domnmuln0rd.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		domnmuln0rd.z	$⊢ \underset{˙}{0} = 0_{R}$
4		domnmuln0rd.1	$⊢ φ \to R \in Domn$
5		domnmuln0rd.2	$⊢ φ \to X \in B$
6		domnmuln0rd.3	$⊢ φ \to Y \in B$
7		domnmuln0rd.4	$⊢ φ \to X \underset{˙}{\cdot} Y \neq \underset{˙}{0}$
8	1 2 3	domneq0	$⊢ (R \in Domn \land X \in B \land Y \in B) \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow (X = \underset{˙}{0} \lor Y = \underset{˙}{0}))$
9	4 5 6 8	syl3anc	$⊢ φ \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow (X = \underset{˙}{0} \lor Y = \underset{˙}{0}))$
10	9	necon3abid	$⊢ φ \to (X \underset{˙}{\cdot} Y \neq \underset{˙}{0} \leftrightarrow \neg (X = \underset{˙}{0} \lor Y = \underset{˙}{0}))$
11	7 10	mpbid	$⊢ φ \to \neg (X = \underset{˙}{0} \lor Y = \underset{˙}{0})$
12		ioran	$⊢ \neg (X = \underset{˙}{0} \lor Y = \underset{˙}{0}) \leftrightarrow (\neg X = \underset{˙}{0} \land \neg Y = \underset{˙}{0})$
13	11 12	sylib	$⊢ φ \to (\neg X = \underset{˙}{0} \land \neg Y = \underset{˙}{0})$
14		neqne	$⊢ \neg X = \underset{˙}{0} \to X \neq \underset{˙}{0}$
15		neqne	$⊢ \neg Y = \underset{˙}{0} \to Y \neq \underset{˙}{0}$
16	14 15	anim12i	$⊢ (\neg X = \underset{˙}{0} \land \neg Y = \underset{˙}{0}) \to (X \neq \underset{˙}{0} \land Y \neq \underset{˙}{0})$
17	13 16	syl	$⊢ φ \to (X \neq \underset{˙}{0} \land Y \neq \underset{˙}{0})$

Metamath Proof Explorer