This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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