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 ‘ 𝑅 ) )