This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )