Theorem domneq0r

Description: Right multiplication by a nonzero element does not change zeroness in a domain. Compare rrgeq0 . (Contributed by SN, 21-Jun-2025)

	Ref	Expression
Hypotheses	domneq0r.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	domneq0r.0	⊢ 0 = ( 0g ‘ 𝑅 )
	domneq0r.m	⊢ · = ( .r ‘ 𝑅 )
	domneq0r.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	domneq0r.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ∖ { 0 } ) )
	domneq0r.r	⊢ ( 𝜑 → 𝑅 ∈ Domn )
Assertion	domneq0r	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ 𝑋 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		domneq0r.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		domneq0r.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		domneq0r.m	⊢ · = ( .r ‘ 𝑅 )
4		domneq0r.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		domneq0r.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ∖ { 0 } ) )
6		domneq0r.r	⊢ ( 𝜑 → 𝑅 ∈ Domn )
7		domnring	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
8	6 7	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
9	5	eldifad	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10	1 3 2 8 9	ringlzd	⊢ ( 𝜑 → ( 0 · 𝑌 ) = 0 )
11	10	eqeq2d	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = ( 0 · 𝑌 ) ↔ ( 𝑋 · 𝑌 ) = 0 ) )
12	1 2	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
13	8 12	syl	⊢ ( 𝜑 → 0 ∈ 𝐵 )
14	1 2 3 4 13 5 6	domnrcanb	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = ( 0 · 𝑌 ) ↔ 𝑋 = 0 ) )
15	11 14	bitr3d	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ 𝑋 = 0 ) )