Step |
Hyp |
Ref |
Expression |
1 |
|
opprdrng.1 |
|- O = ( oppR ` R ) |
2 |
1
|
opprringb |
|- ( R e. Ring <-> O e. Ring ) |
3 |
2
|
anbi1i |
|- ( ( R e. Ring /\ ( Unit ` R ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) ) <-> ( O e. Ring /\ ( Unit ` R ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) ) ) |
4 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
5 |
|
eqid |
|- ( Unit ` R ) = ( Unit ` R ) |
6 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
7 |
4 5 6
|
isdrng |
|- ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) ) ) |
8 |
1 4
|
opprbas |
|- ( Base ` R ) = ( Base ` O ) |
9 |
5 1
|
opprunit |
|- ( Unit ` R ) = ( Unit ` O ) |
10 |
1 6
|
oppr0 |
|- ( 0g ` R ) = ( 0g ` O ) |
11 |
8 9 10
|
isdrng |
|- ( O e. DivRing <-> ( O e. Ring /\ ( Unit ` R ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) ) ) |
12 |
3 7 11
|
3bitr4i |
|- ( R e. DivRing <-> O e. DivRing ) |