Step |
Hyp |
Ref |
Expression |
1 |
|
0ringdif.b |
|- B = ( Base ` R ) |
2 |
|
0ringdif.0 |
|- .0. = ( 0g ` R ) |
3 |
|
0ring1eq0.1 |
|- .1. = ( 1r ` R ) |
4 |
|
eldif |
|- ( R e. ( Ring \ NzRing ) <-> ( R e. Ring /\ -. R e. NzRing ) ) |
5 |
|
0ringnnzr |
|- ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 <-> -. R e. NzRing ) ) |
6 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
7 |
6 2 3
|
0ring01eq |
|- ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> .0. = .1. ) |
8 |
7
|
eqcomd |
|- ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> .1. = .0. ) |
9 |
8
|
ex |
|- ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 -> .1. = .0. ) ) |
10 |
5 9
|
sylbird |
|- ( R e. Ring -> ( -. R e. NzRing -> .1. = .0. ) ) |
11 |
10
|
imp |
|- ( ( R e. Ring /\ -. R e. NzRing ) -> .1. = .0. ) |
12 |
4 11
|
sylbi |
|- ( R e. ( Ring \ NzRing ) -> .1. = .0. ) |