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 B = Base R
drngmuleq0.o 0 ˙ = 0 R
drngmuleq0.t · ˙ = R
drngmuleq0.r φ R DivRing
drngmuleq0.x φ X B
drngmuleq0.y φ Y B
Assertion drngmulne0 φ X · ˙ Y 0 ˙ X 0 ˙ Y 0 ˙

Proof

Step Hyp Ref Expression
1 drngmuleq0.b B = Base R
2 drngmuleq0.o 0 ˙ = 0 R
3 drngmuleq0.t · ˙ = R
4 drngmuleq0.r φ R DivRing
5 drngmuleq0.x φ X B
6 drngmuleq0.y φ Y B
7 1 2 3 4 5 6 drngmul0or φ X · ˙ Y = 0 ˙ X = 0 ˙ Y = 0 ˙
8 7 necon3abid φ X · ˙ Y 0 ˙ ¬ X = 0 ˙ Y = 0 ˙
9 neanior X 0 ˙ Y 0 ˙ ¬ X = 0 ˙ Y = 0 ˙
10 8 9 bitr4di φ X · ˙ Y 0 ˙ X 0 ˙ Y 0 ˙