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

Metamath Proof Explorer

Theorem unitnz

Description: In a nonzero ring, a unit cannot be zero. (Contributed by Thierry Arnoux, 25-Apr-2025)

Ref Expression
Hypotheses unitnz.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
unitnz.2 ⊢ 0 = ( 0g ‘ 𝑅 )
unitnz.3 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
unitnz.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
Assertion unitnz ( 𝜑 → 𝑋 ≠ 0 )

Proof

Step Hyp Ref Expression
1 unitnz.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
2 unitnz.2 ⊢ 0 = ( 0g ‘ 𝑅 )
3 unitnz.3 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
4 unitnz.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
5 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
6 3 5 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8 7 2 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
9 3 8 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ 0 )
10 1 2 7 0unit ⊢ ( 𝑅 ∈ Ring → ( 0 ∈ 𝑈 ↔ ( 1r ‘ 𝑅 ) = 0 ) )
11 10 necon3bbid ⊢ ( 𝑅 ∈ Ring → ( ¬ 0 ∈ 𝑈 ↔ ( 1r ‘ 𝑅 ) ≠ 0 ) )
12 11 biimpar ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ 0 ) → ¬ 0 ∈ 𝑈 )
13 6 9 12 syl2anc ⊢ ( 𝜑 → ¬ 0 ∈ 𝑈 )
14 nelne2 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ ¬ 0 ∈ 𝑈 ) → 𝑋 ≠ 0 )
15 4 13 14 syl2anc ⊢ ( 𝜑 → 𝑋 ≠ 0 )