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

Metamath Proof Explorer

Theorem ringunitnzdiv

Description: In a unitary ring, a unit 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 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
ringunitnzdiv.x ⊢ ( 𝜑 → 𝑋 ∈ ( Unit ‘ 𝑅 ) )
Assertion ringunitnzdiv ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 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 ringunitnzdiv.x ⊢ ( 𝜑 → 𝑋 ∈ ( Unit ‘ 𝑅 ) )
7 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
9 1 8 unitcl ⊢ ( 𝑋 ∈ ( Unit ‘ 𝑅 ) → 𝑋 ∈ 𝐵 )
10 6 9 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
12 8 11 1 ringinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) ∈ 𝐵 )
13 4 6 12 syl2anc ⊢ ( 𝜑 → ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) ∈ 𝐵 )
14 oveq1 ⊢ ( 𝑒 = ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) → ( 𝑒 · 𝑋 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) · 𝑋 ) )
15 14 eqeq1d ⊢ ( 𝑒 = ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) → ( ( 𝑒 · 𝑋 ) = ( 1r ‘ 𝑅 ) ↔ ( ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) · 𝑋 ) = ( 1r ‘ 𝑅 ) ) )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑒 = ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) ) → ( ( 𝑒 · 𝑋 ) = ( 1r ‘ 𝑅 ) ↔ ( ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) · 𝑋 ) = ( 1r ‘ 𝑅 ) ) )
17 8 11 3 7 unitlinv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) · 𝑋 ) = ( 1r ‘ 𝑅 ) )
18 4 6 17 syl2anc ⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) · 𝑋 ) = ( 1r ‘ 𝑅 ) )
19 13 16 18 rspcedvd ⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ( 𝑒 · 𝑋 ) = ( 1r ‘ 𝑅 ) )
20 1 3 7 2 4 10 19 5 ringinvnzdiv ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ 𝑌 = 0 ) )