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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	domnmuln0rd.t	⊢ · = ( .r ‘ 𝑅 )
	domnmuln0rd.z	⊢ 0 = ( 0g ‘ 𝑅 )
	domnmuln0rd.1	⊢ ( 𝜑 → 𝑅 ∈ Domn )
	domnmuln0rd.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	domnmuln0rd.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	domnmuln0rd.4	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ≠ 0 )
Assertion	domnmuln0rd	⊢ ( 𝜑 → ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		domnmuln0rd.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		domnmuln0rd.t	⊢ · = ( .r ‘ 𝑅 )
3		domnmuln0rd.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		domnmuln0rd.1	⊢ ( 𝜑 → 𝑅 ∈ Domn )
5		domnmuln0rd.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		domnmuln0rd.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		domnmuln0rd.4	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ≠ 0 )
8	1 2 3	domneq0	⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
9	4 5 6 8	syl3anc	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
10	9	necon3abid	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ¬ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
11	7 10	mpbid	⊢ ( 𝜑 → ¬ ( 𝑋 = 0 ∨ 𝑌 = 0 ) )
12		ioran	⊢ ( ¬ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ↔ ( ¬ 𝑋 = 0 ∧ ¬ 𝑌 = 0 ) )
13	11 12	sylib	⊢ ( 𝜑 → ( ¬ 𝑋 = 0 ∧ ¬ 𝑌 = 0 ) )
14		neqne	⊢ ( ¬ 𝑋 = 0 → 𝑋 ≠ 0 )
15		neqne	⊢ ( ¬ 𝑌 = 0 → 𝑌 ≠ 0 )
16	14 15	anim12i	⊢ ( ( ¬ 𝑋 = 0 ∧ ¬ 𝑌 = 0 ) → ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) )
17	13 16	syl	⊢ ( 𝜑 → ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) )