opprnzr

Description: The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015)

		Ref	Expression
	Hypothesis	opprnzr.1	$⊢ O = {opp}_{r} (R)$
	Assertion	opprnzr	$⊢ R \in NzRing \to O \in NzRing$

Step	Hyp	Ref	Expression
1		opprnzr.1	$⊢ O = {opp}_{r} (R)$
2		nzrring	$⊢ R \in NzRing \to R \in Ring$
3	1	opprring	$⊢ R \in Ring \to O \in Ring$
4	2 3	syl	$⊢ R \in NzRing \to O \in Ring$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	5	isnzr2	$⊢ R \in NzRing \leftrightarrow (R \in Ring \land 2_{𝑜} ≼ {Base}_{R})$
7	6	simprbi	$⊢ R \in NzRing \to 2_{𝑜} ≼ {Base}_{R}$
8	1 5	opprbas	$⊢ {Base}_{R} = {Base}_{O}$
9	8	isnzr2	$⊢ O \in NzRing \leftrightarrow (O \in Ring \land 2_{𝑜} ≼ {Base}_{R})$
10	4 7 9	sylanbrc	$⊢ R \in NzRing \to O \in NzRing$

Metamath Proof Explorer