Step |
Hyp |
Ref |
Expression |
1 |
|
ringelnzr.z |
|- .0. = ( 0g ` R ) |
2 |
|
ringelnzr.b |
|- B = ( Base ` R ) |
3 |
|
simpl |
|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> R e. Ring ) |
4 |
|
eldifsni |
|- ( X e. ( B \ { .0. } ) -> X =/= .0. ) |
5 |
4
|
adantl |
|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> X =/= .0. ) |
6 |
|
eldifi |
|- ( X e. ( B \ { .0. } ) -> X e. B ) |
7 |
6
|
adantl |
|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> X e. B ) |
8 |
2 1
|
ring0cl |
|- ( R e. Ring -> .0. e. B ) |
9 |
8
|
adantr |
|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> .0. e. B ) |
10 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
11 |
2 10 1
|
ring1eq0 |
|- ( ( R e. Ring /\ X e. B /\ .0. e. B ) -> ( ( 1r ` R ) = .0. -> X = .0. ) ) |
12 |
3 7 9 11
|
syl3anc |
|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> ( ( 1r ` R ) = .0. -> X = .0. ) ) |
13 |
12
|
necon3d |
|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> ( X =/= .0. -> ( 1r ` R ) =/= .0. ) ) |
14 |
5 13
|
mpd |
|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> ( 1r ` R ) =/= .0. ) |
15 |
10 1
|
isnzr |
|- ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= .0. ) ) |
16 |
3 14 15
|
sylanbrc |
|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> R e. NzRing ) |