Metamath Proof Explorer


Theorem drngmulne0

Description: A product is nonzero iff both its factors are nonzero. (Contributed by NM, 18-Oct-2014)

Ref Expression
Hypotheses drngmuleq0.b 𝐵 = ( Base ‘ 𝑅 )
drngmuleq0.o 0 = ( 0g𝑅 )
drngmuleq0.t · = ( .r𝑅 )
drngmuleq0.r ( 𝜑𝑅 ∈ DivRing )
drngmuleq0.x ( 𝜑𝑋𝐵 )
drngmuleq0.y ( 𝜑𝑌𝐵 )
Assertion drngmulne0 ( 𝜑 → ( ( 𝑋 · 𝑌 ) ≠ 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 1 2 3 4 5 6 drngmul0or ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0𝑌 = 0 ) ) )
8 7 necon3abid ( 𝜑 → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ¬ ( 𝑋 = 0𝑌 = 0 ) ) )
9 neanior ( ( 𝑋0𝑌0 ) ↔ ¬ ( 𝑋 = 0𝑌 = 0 ) )
10 8 9 bitr4di ( 𝜑 → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ( 𝑋0𝑌0 ) ) )