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 \in NzRing \to {inv}_{g} (R) (1_{R}) \neq 0_{R}$

Step	Hyp	Ref	Expression
1		nzrring	$⊢ R \in NzRing \to R \in Ring$
2		eqid	$⊢ Unit (R) = Unit (R)$
3		eqid	$⊢ 1_{R} = 1_{R}$
4	2 3	1unit	$⊢ R \in Ring \to 1_{R} \in Unit (R)$
5		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
6	2 5	unitnegcl	$⊢ (R \in Ring \land 1_{R} \in Unit (R)) \to {inv}_{g} (R) (1_{R}) \in Unit (R)$
7	1 4 6	syl2anc2	$⊢ R \in NzRing \to {inv}_{g} (R) (1_{R}) \in Unit (R)$
8		eqid	$⊢ 0_{R} = 0_{R}$
9	2 8	nzrunit	$⊢ (R \in NzRing \land {inv}_{g} (R) (1_{R}) \in Unit (R)) \to {inv}_{g} (R) (1_{R}) \neq 0_{R}$
10	7 9	mpdan	$⊢ R \in NzRing \to {inv}_{g} (R) (1_{R}) \neq 0_{R}$

Metamath Proof Explorer