Metamath Proof Explorer

Theorem drngmxidl

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

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

Proof

Step Hyp Ref Expression
1 drngmxidl.1 
 |-  .0. = ( 0g ` R )
2 drngring 
 |-  ( R e. DivRing -> R e. Ring )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 3 mxidlidl 
 |-  ( ( R e. Ring /\ i e. ( MaxIdeal ` R ) ) -> i e. ( LIdeal ` R ) )
5 4 ex 
 |-  ( R e. Ring -> ( i e. ( MaxIdeal ` R ) -> i e. ( LIdeal ` R ) ) )
6 5 ssrdv 
 |-  ( R e. Ring -> ( MaxIdeal ` R ) C_ ( LIdeal ` R ) )
7 2 6 syl 
 |-  ( R e. DivRing -> ( MaxIdeal ` R ) C_ ( LIdeal ` R ) )
8 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
9 3 1 8 drngnidl 
 |-  ( R e. DivRing -> ( LIdeal ` R ) = { { .0. } , ( Base ` R ) } )
10 7 9 sseqtrd 
 |-  ( R e. DivRing -> ( MaxIdeal ` R ) C_ { { .0. } , ( Base ` R ) } )
11 3 mxidlnr 
 |-  ( ( R e. Ring /\ i e. ( MaxIdeal ` R ) ) -> i =/= ( Base ` R ) )
12 2 11 sylan 
 |-  ( ( R e. DivRing /\ i e. ( MaxIdeal ` R ) ) -> i =/= ( Base ` R ) )
13 12 nelrdva 
 |-  ( R e. DivRing -> -. ( Base ` R ) e. ( MaxIdeal ` R ) )
14 ssdifsn 
 |-  ( ( MaxIdeal ` R ) C_ ( { { .0. } , ( Base ` R ) } \ { ( Base ` R ) } ) <-> ( ( MaxIdeal ` R ) C_ { { .0. } , ( Base ` R ) } /\ -. ( Base ` R ) e. ( MaxIdeal ` R ) ) )
15 10 13 14 sylanbrc 
 |-  ( R e. DivRing -> ( MaxIdeal ` R ) C_ ( { { .0. } , ( Base ` R ) } \ { ( Base ` R ) } ) )
16 drngnzr 
 |-  ( R e. DivRing -> R e. NzRing )
17 1 3 drnglidl1ne0 
 |-  ( R e. NzRing -> ( Base ` R ) =/= { .0. } )
18 17 necomd 
 |-  ( R e. NzRing -> { .0. } =/= ( Base ` R ) )
19 difprsn2 
 |-  ( { .0. } =/= ( Base ` R ) -> ( { { .0. } , ( Base ` R ) } \ { ( Base ` R ) } ) = { { .0. } } )
20 16 18 19 3syl 
 |-  ( R e. DivRing -> ( { { .0. } , ( Base ` R ) } \ { ( Base ` R ) } ) = { { .0. } } )
21 15 20 sseqtrd 
 |-  ( R e. DivRing -> ( MaxIdeal ` R ) C_ { { .0. } } )
22 1 drng0mxidl 
 |-  ( R e. DivRing -> { .0. } e. ( MaxIdeal ` R ) )
23 22 snssd 
 |-  ( R e. DivRing -> { { .0. } } C_ ( MaxIdeal ` R ) )
24 21 23 eqssd 
 |-  ( R e. DivRing -> ( MaxIdeal ` R ) = { { .0. } } )