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