Theorem drngmul0or

Description: A product is zero iff one of its factors is zero. (Contributed by NM, 8-Oct-2014) (Proof shortened by SN, 25-Jun-2025)

	Ref	Expression
Hypotheses	drngmuleq0.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	drngmuleq0.o	⊢ 0 = ( 0g ‘ 𝑅 )
	drngmuleq0.t	⊢ · = ( .r ‘ 𝑅 )
	drngmuleq0.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
	drngmuleq0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	drngmuleq0.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	drngmul0or	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		drngmuleq0.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		drngmuleq0.o	⊢ 0 = ( 0g ‘ 𝑅 )
3		drngmuleq0.t	⊢ · = ( .r ‘ 𝑅 )
4		drngmuleq0.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
5		drngmuleq0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		drngmuleq0.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		drngdomn	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Domn )
8	4 7	syl	⊢ ( 𝜑 → 𝑅 ∈ Domn )
9	1 3 2	domneq0	⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
10	8 5 6 9	syl3anc	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )