Step |
Hyp |
Ref |
Expression |
1 |
|
mxidlval.1 |
|- B = ( Base ` R ) |
2 |
1
|
mxidlidl |
|- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) |
3 |
|
eqid |
|- ( LIdeal ` R ) = ( LIdeal ` R ) |
4 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
5 |
3 4
|
lidl0cl |
|- ( ( R e. Ring /\ M e. ( LIdeal ` R ) ) -> ( 0g ` R ) e. M ) |
6 |
2 5
|
syldan |
|- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( 0g ` R ) e. M ) |
7 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
8 |
1 7
|
mxidln1 |
|- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> -. ( 1r ` R ) e. M ) |
9 |
|
nelne2 |
|- ( ( ( 0g ` R ) e. M /\ -. ( 1r ` R ) e. M ) -> ( 0g ` R ) =/= ( 1r ` R ) ) |
10 |
6 8 9
|
syl2anc |
|- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( 0g ` R ) =/= ( 1r ` R ) ) |
11 |
10
|
necomd |
|- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( 1r ` R ) =/= ( 0g ` R ) ) |
12 |
7 4
|
isnzr |
|- ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) ) |
13 |
12
|
biimpri |
|- ( ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> R e. NzRing ) |
14 |
11 13
|
syldan |
|- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> R e. NzRing ) |