opprnzrb

Description: The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr . (Contributed by SN, 20-Jun-2025)

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

Step	Hyp	Ref	Expression
1		opprnzr.1	$⊢ O = {opp}_{r} (R)$
2	1	opprringb	$⊢ R \in Ring \leftrightarrow O \in Ring$
3	2	anbi1i	$⊢ (R \in Ring \land 1_{R} \neq 0_{R}) \leftrightarrow (O \in Ring \land 1_{R} \neq 0_{R})$
4		eqid	$⊢ 1_{R} = 1_{R}$
5		eqid	$⊢ 0_{R} = 0_{R}$
6	4 5	isnzr	$⊢ R \in NzRing \leftrightarrow (R \in Ring \land 1_{R} \neq 0_{R})$
7	1 4	oppr1	$⊢ 1_{R} = 1_{O}$
8	1 5	oppr0	$⊢ 0_{R} = 0_{O}$
9	7 8	isnzr	$⊢ O \in NzRing \leftrightarrow (O \in Ring \land 1_{R} \neq 0_{R})$
10	3 6 9	3bitr4i	$⊢ R \in NzRing \leftrightarrow O \in NzRing$

Metamath Proof Explorer