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 B = Base R
drngmuleq0.o 0 ˙ = 0 R
drngmuleq0.t · ˙ = R
drngmuleq0.r φ R DivRing
drngmuleq0.x φ X B
drngmuleq0.y φ Y B
drngmuleq0.e φ Y 0 ˙
Assertion drngmuleq0 φ X · ˙ Y = 0 ˙ X = 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 drngmuleq0.e φ Y 0 ˙
8 1 2 3 4 5 6 drngmul0or φ X · ˙ Y = 0 ˙ X = 0 ˙ Y = 0 ˙
9 df-ne Y 0 ˙ ¬ Y = 0 ˙
10 orel2 ¬ Y = 0 ˙ X = 0 ˙ Y = 0 ˙ X = 0 ˙
11 orc X = 0 ˙ X = 0 ˙ Y = 0 ˙
12 10 11 impbid1 ¬ Y = 0 ˙ X = 0 ˙ Y = 0 ˙ X = 0 ˙
13 9 12 sylbi Y 0 ˙ X = 0 ˙ Y = 0 ˙ X = 0 ˙
14 7 13 syl φ X = 0 ˙ Y = 0 ˙ X = 0 ˙
15 8 14 bitrd φ X · ˙ Y = 0 ˙ X = 0 ˙