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

Metamath Proof Explorer

Theorem ring1nzdiv

Description: In a unitary ring, the ring unity is not a zero divisor. (Contributed by AV, 7-Mar-2025)

Ref Expression
Hypotheses ringunitnzdiv.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ringunitnzdiv.z ⊢ 0 = ( 0g ‘ 𝑅 )
ringunitnzdiv.t ⊢ · = ( .r ‘ 𝑅 )
ringunitnzdiv.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
ringunitnzdiv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
ring1nzdiv.x ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion ring1nzdiv ( 𝜑 → ( ( 1 · 𝑌 ) = 0 ↔ 𝑌 = 0 ) )

Proof

Step Hyp Ref Expression
1 ringunitnzdiv.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ringunitnzdiv.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 ringunitnzdiv.t ⊢ · = ( .r ‘ 𝑅 )
4 ringunitnzdiv.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 ringunitnzdiv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 ring1nzdiv.x ⊢ 1 = ( 1r ‘ 𝑅 )
7 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
8 7 6 1unit ⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Unit ‘ 𝑅 ) )
9 4 8 syl ⊢ ( 𝜑 → 1 ∈ ( Unit ‘ 𝑅 ) )
10 1 2 3 4 5 9 ringunitnzdiv ⊢ ( 𝜑 → ( ( 1 · 𝑌 ) = 0 ↔ 𝑌 = 0 ) )