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

Metamath Proof Explorer

Theorem drng0mxidl

Description: In a division ring, the zero ideal is a maximal ideal. (Contributed by Thierry Arnoux, 16-Mar-2025)

Ref Expression
Hypothesis drngmxidl.1 
|- .0. = ( 0g ` R )
Assertion drng0mxidl 
|- ( R e. DivRing -> { .0. } e. ( MaxIdeal ` R ) )

Proof

Step Hyp Ref Expression
1 drngmxidl.1 
 |-  .0. = ( 0g ` R )
2 drngring 
 |-  ( R e. DivRing -> R e. Ring )
3 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
4 3 1 lidl0 
 |-  ( R e. Ring -> { .0. } e. ( LIdeal ` R ) )
5 2 4 syl 
 |-  ( R e. DivRing -> { .0. } e. ( LIdeal ` R ) )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
8 6 7 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
9 2 8 syl 
 |-  ( R e. DivRing -> ( 1r ` R ) e. ( Base ` R ) )
10 drngnzr 
 |-  ( R e. DivRing -> R e. NzRing )
11 7 1 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= .0. )
12 nelsn 
 |-  ( ( 1r ` R ) =/= .0. -> -. ( 1r ` R ) e. { .0. } )
13 10 11 12 3syl 
 |-  ( R e. DivRing -> -. ( 1r ` R ) e. { .0. } )
14 nelne1 
 |-  ( ( ( 1r ` R ) e. ( Base ` R ) /\ -. ( 1r ` R ) e. { .0. } ) -> ( Base ` R ) =/= { .0. } )
15 9 13 14 syl2anc 
 |-  ( R e. DivRing -> ( Base ` R ) =/= { .0. } )
16 15 necomd 
 |-  ( R e. DivRing -> { .0. } =/= ( Base ` R ) )
17 6 1 3 drngnidl 
 |-  ( R e. DivRing -> ( LIdeal ` R ) = { { .0. } , ( Base ` R ) } )
18 17 eleq2d 
 |-  ( R e. DivRing -> ( j e. ( LIdeal ` R ) <-> j e. { { .0. } , ( Base ` R ) } ) )
19 18 biimpa 
 |-  ( ( R e. DivRing /\ j e. ( LIdeal ` R ) ) -> j e. { { .0. } , ( Base ` R ) } )
20 elpri 
 |-  ( j e. { { .0. } , ( Base ` R ) } -> ( j = { .0. } \/ j = ( Base ` R ) ) )
21 19 20 syl 
 |-  ( ( R e. DivRing /\ j e. ( LIdeal ` R ) ) -> ( j = { .0. } \/ j = ( Base ` R ) ) )
22 21 a1d 
 |-  ( ( R e. DivRing /\ j e. ( LIdeal ` R ) ) -> ( { .0. } C_ j -> ( j = { .0. } \/ j = ( Base ` R ) ) ) )
23 22 ralrimiva 
 |-  ( R e. DivRing -> A. j e. ( LIdeal ` R ) ( { .0. } C_ j -> ( j = { .0. } \/ j = ( Base ` R ) ) ) )
24 6 ismxidl 
 |-  ( R e. Ring -> ( { .0. } e. ( MaxIdeal ` R ) <-> ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( { .0. } C_ j -> ( j = { .0. } \/ j = ( Base ` R ) ) ) ) ) )
25 24 biimpar 
 |-  ( ( R e. Ring /\ ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( { .0. } C_ j -> ( j = { .0. } \/ j = ( Base ` R ) ) ) ) ) -> { .0. } e. ( MaxIdeal ` R ) )
26 2 5 16 23 25 syl13anc 
 |-  ( R e. DivRing -> { .0. } e. ( MaxIdeal ` R ) )