This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 = ( oppR ` R )
Assertion opprnzrb 
|- ( R e. NzRing <-> O e. NzRing )

Proof

Step Hyp Ref Expression
1 opprnzr.1 
 |-  O = ( oppR ` R )
2 1 opprringb 
 |-  ( R e. Ring <-> O e. Ring )
3 2 anbi1i 
 |-  ( ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) <-> ( O e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) )
4 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
5 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
6 4 5 isnzr 
 |-  ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) )
7 1 4 oppr1 
 |-  ( 1r ` R ) = ( 1r ` O )
8 1 5 oppr0 
 |-  ( 0g ` R ) = ( 0g ` O )
9 7 8 isnzr 
 |-  ( O e. NzRing <-> ( O e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) )
10 3 6 9 3bitr4i 
 |-  ( R e. NzRing <-> O e. NzRing )