Metamath Proof Explorer

Theorem drngmxidlr

Description: If a ring's only maximal ideal is the zero ideal, it is a division ring. See also drngmxidl . (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypotheses drngmxidlr.b 
|- B = ( Base ` R )
drngmxidlr.z 
|- .0. = ( 0g ` R )
drngmxidlr.u 
|- M = ( MaxIdeal ` R )
drngmxidlr.r 
|- ( ph -> R e. NzRing )
drngmxidlr.2 
|- ( ph -> M = { { .0. } } )
Assertion drngmxidlr 
|- ( ph -> R e. DivRing )

Proof

Step Hyp Ref Expression
1 drngmxidlr.b 
 |-  B = ( Base ` R )
2 drngmxidlr.z 
 |-  .0. = ( 0g ` R )
3 drngmxidlr.u 
 |-  M = ( MaxIdeal ` R )
4 drngmxidlr.r 
 |-  ( ph -> R e. NzRing )
5 drngmxidlr.2 
 |-  ( ph -> M = { { .0. } } )
6 simpr 
 |-  ( ( ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ i C_ m ) -> i C_ m )
7 simplr 
 |-  ( ( ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ i C_ m ) -> m e. ( MaxIdeal ` R ) )
8 7 3 eleqtrrdi 
 |-  ( ( ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ i C_ m ) -> m e. M )
9 5 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ i C_ m ) -> M = { { .0. } } )
10 8 9 eleqtrd 
 |-  ( ( ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ i C_ m ) -> m e. { { .0. } } )
11 elsni 
 |-  ( m e. { { .0. } } -> m = { .0. } )
12 10 11 syl 
 |-  ( ( ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ i C_ m ) -> m = { .0. } )
13 6 12 sseqtrd 
 |-  ( ( ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ i C_ m ) -> i C_ { .0. } )
14 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
15 4 14 syl 
 |-  ( ph -> R e. Ring )
16 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
17 16 2 lidl0cl 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) -> .0. e. i )
18 15 17 sylan 
 |-  ( ( ph /\ i e. ( LIdeal ` R ) ) -> .0. e. i )
19 18 snssd 
 |-  ( ( ph /\ i e. ( LIdeal ` R ) ) -> { .0. } C_ i )
20 19 ad5ant12 
 |-  ( ( ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ i C_ m ) -> { .0. } C_ i )
21 13 20 eqssd 
 |-  ( ( ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ i C_ m ) -> i = { .0. } )
22 15 ad2antrr 
 |-  ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) -> R e. Ring )
23 simplr 
 |-  ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) -> i e. ( LIdeal ` R ) )
24 simpr 
 |-  ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) -> i =/= B )
25 1 ssmxidl 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) /\ i =/= B ) -> E. m e. ( MaxIdeal ` R ) i C_ m )
26 22 23 24 25 syl3anc 
 |-  ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) -> E. m e. ( MaxIdeal ` R ) i C_ m )
27 21 26 r19.29a 
 |-  ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i =/= B ) -> i = { .0. } )
28 simpr 
 |-  ( ( ( ph /\ i e. ( LIdeal ` R ) ) /\ i = B ) -> i = B )
29 exmidne 
 |-  ( i = B \/ i =/= B )
30 29 a1i 
 |-  ( ( ph /\ i e. ( LIdeal ` R ) ) -> ( i = B \/ i =/= B ) )
31 30 orcomd 
 |-  ( ( ph /\ i e. ( LIdeal ` R ) ) -> ( i =/= B \/ i = B ) )
32 27 28 31 orim12da 
 |-  ( ( ph /\ i e. ( LIdeal ` R ) ) -> ( i = { .0. } \/ i = B ) )
33 vex 
 |-  i e. _V
34 33 elpr 
 |-  ( i e. { { .0. } , B } <-> ( i = { .0. } \/ i = B ) )
35 32 34 sylibr 
 |-  ( ( ph /\ i e. ( LIdeal ` R ) ) -> i e. { { .0. } , B } )
36 35 ex 
 |-  ( ph -> ( i e. ( LIdeal ` R ) -> i e. { { .0. } , B } ) )
37 36 ssrdv 
 |-  ( ph -> ( LIdeal ` R ) C_ { { .0. } , B } )
38 16 2 lidl0 
 |-  ( R e. Ring -> { .0. } e. ( LIdeal ` R ) )
39 15 38 syl 
 |-  ( ph -> { .0. } e. ( LIdeal ` R ) )
40 16 1 lidl1 
 |-  ( R e. Ring -> B e. ( LIdeal ` R ) )
41 15 40 syl 
 |-  ( ph -> B e. ( LIdeal ` R ) )
42 39 41 prssd 
 |-  ( ph -> { { .0. } , B } C_ ( LIdeal ` R ) )
43 37 42 eqssd 
 |-  ( ph -> ( LIdeal ` R ) = { { .0. } , B } )
44 1 2 16 drngidl 
 |-  ( R e. NzRing -> ( R e. DivRing <-> ( LIdeal ` R ) = { { .0. } , B } ) )
45 4 44 syl 
 |-  ( ph -> ( R e. DivRing <-> ( LIdeal ` R ) = { { .0. } , B } ) )
46 43 45 mpbird 
 |-  ( ph -> R e. DivRing )