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 
|- U = ( Unit ` R )
unitnz.2 
|- .0. = ( 0g ` R )
unitnz.3 
|- ( ph -> R e. NzRing )
unitnz.4 
|- ( ph -> X e. U )
Assertion unitnz 
|- ( ph -> X =/= .0. )

Proof

Step Hyp Ref Expression
1 unitnz.1 
 |-  U = ( Unit ` R )
2 unitnz.2 
 |-  .0. = ( 0g ` R )
3 unitnz.3 
 |-  ( ph -> R e. NzRing )
4 unitnz.4 
 |-  ( ph -> X e. U )
5 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
6 3 5 syl 
 |-  ( ph -> R e. Ring )
7 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
8 7 2 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= .0. )
9 3 8 syl 
 |-  ( ph -> ( 1r ` R ) =/= .0. )
10 1 2 7 0unit 
 |-  ( R e. Ring -> ( .0. e. U <-> ( 1r ` R ) = .0. ) )
11 10 necon3bbid 
 |-  ( R e. Ring -> ( -. .0. e. U <-> ( 1r ` R ) =/= .0. ) )
12 11 biimpar 
 |-  ( ( R e. Ring /\ ( 1r ` R ) =/= .0. ) -> -. .0. e. U )
13 6 9 12 syl2anc 
 |-  ( ph -> -. .0. e. U )
14 nelne2 
 |-  ( ( X e. U /\ -. .0. e. U ) -> X =/= .0. )
15 4 13 14 syl2anc 
 |-  ( ph -> X =/= .0. )