Metamath Proof Explorer


Theorem mxidlnzr

Description: A ring with a maximal ideal is a nonzero ring. (Contributed by Jeff Madsen, 17-Jun-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Hypothesis mxidlval.1
|- B = ( Base ` R )
Assertion mxidlnzr
|- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> R e. NzRing )

Proof

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 )