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 ( 𝑅 ∈ NzRing → ( ( invg𝑅 ) ‘ ( 1r𝑅 ) ) ≠ ( 0g𝑅 ) )

Proof

Step Hyp Ref Expression
1 nzrring ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
2 eqid ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
3 eqid ( 1r𝑅 ) = ( 1r𝑅 )
4 2 3 1unit ( 𝑅 ∈ Ring → ( 1r𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
5 eqid ( invg𝑅 ) = ( invg𝑅 )
6 2 5 unitnegcl ( ( 𝑅 ∈ Ring ∧ ( 1r𝑅 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( invg𝑅 ) ‘ ( 1r𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
7 1 4 6 syl2anc2 ( 𝑅 ∈ NzRing → ( ( invg𝑅 ) ‘ ( 1r𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
8 eqid ( 0g𝑅 ) = ( 0g𝑅 )
9 2 8 nzrunit ( ( 𝑅 ∈ NzRing ∧ ( ( invg𝑅 ) ‘ ( 1r𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( invg𝑅 ) ‘ ( 1r𝑅 ) ) ≠ ( 0g𝑅 ) )
10 7 9 mpdan ( 𝑅 ∈ NzRing → ( ( invg𝑅 ) ‘ ( 1r𝑅 ) ) ≠ ( 0g𝑅 ) )