Metamath Proof Explorer

Theorem nzrneg1ne0

Description: The additive inverse of the 1 in a nonzero ring is not zero ( -1 =/= 0 ). (Contributed by AV, 29-Apr-2019)

Ref Expression
Assertion nzrneg1ne0 
|- ( R e. NzRing -> ( ( invg ` R ) ` ( 1r ` R ) ) =/= ( 0g ` R ) )

Proof

Step Hyp Ref Expression
1 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
2 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
3 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
4 2 3 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Unit ` R ) )
5 eqid 
 |-  ( invg ` R ) = ( invg ` R )
6 2 5 unitnegcl 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. ( Unit ` R ) ) -> ( ( invg ` R ) ` ( 1r ` R ) ) e. ( Unit ` R ) )
7 1 4 6 syl2anc2 
 |-  ( R e. NzRing -> ( ( invg ` R ) ` ( 1r ` R ) ) e. ( Unit ` R ) )
8 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
9 2 8 nzrunit 
 |-  ( ( R e. NzRing /\ ( ( invg ` R ) ` ( 1r ` R ) ) e. ( Unit ` R ) ) -> ( ( invg ` R ) ` ( 1r ` R ) ) =/= ( 0g ` R ) )
10 7 9 mpdan 
 |-  ( R e. NzRing -> ( ( invg ` R ) ` ( 1r ` R ) ) =/= ( 0g ` R ) )