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

Metamath Proof Explorer

Theorem drngmuleq0

Description: An element is zero iff its product with a nonzero element is zero. (Contributed by NM, 8-Oct-2014)

Ref Expression
Hypotheses drngmuleq0.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
drngmuleq0.o ⊢ 0 = ( 0g ‘ 𝑅 )
drngmuleq0.t ⊢ · = ( .r ‘ 𝑅 )
drngmuleq0.r ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
drngmuleq0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
drngmuleq0.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
drngmuleq0.e ⊢ ( 𝜑 → 𝑌 ≠ 0 )
Assertion drngmuleq0 ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 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 drngmuleq0.e ⊢ ( 𝜑 → 𝑌 ≠ 0 )
8 1 2 3 4 5 6 drngmul0or ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
9 df-ne ⊢ ( 𝑌 ≠ 0 ↔ ¬ 𝑌 = 0 )
10 orel2 ⊢ ( ¬ 𝑌 = 0 → ( ( 𝑋 = 0 ∨ 𝑌 = 0 ) → 𝑋 = 0 ) )
11 orc ⊢ ( 𝑋 = 0 → ( 𝑋 = 0 ∨ 𝑌 = 0 ) )
12 10 11 impbid1 ⊢ ( ¬ 𝑌 = 0 → ( ( 𝑋 = 0 ∨ 𝑌 = 0 ) ↔ 𝑋 = 0 ) )
13 9 12 sylbi ⊢ ( 𝑌 ≠ 0 → ( ( 𝑋 = 0 ∨ 𝑌 = 0 ) ↔ 𝑋 = 0 ) )
14 7 13 syl ⊢ ( 𝜑 → ( ( 𝑋 = 0 ∨ 𝑌 = 0 ) ↔ 𝑋 = 0 ) )
15 8 14 bitrd ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ 𝑋 = 0 ) )