This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )