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

Metamath Proof Explorer

Theorem krullndrng

Description: Krull's theorem for non-division-rings: Existence of a nonzero maximal ideal. (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypotheses krullndrng.1 
|- .0. = ( 0g ` R )
krullndrng.2 
|- ( ph -> R e. NzRing )
krullndrng.3 
|- ( ph -> -. R e. DivRing )
Assertion krullndrng 
|- ( ph -> E. m e. ( MaxIdeal ` R ) m =/= { .0. } )

Proof

Step Hyp Ref Expression
1 krullndrng.1 
 |-  .0. = ( 0g ` R )
2 krullndrng.2 
 |-  ( ph -> R e. NzRing )
3 krullndrng.3 
 |-  ( ph -> -. R e. DivRing )
4 krull 
 |-  ( R e. NzRing -> E. n n e. ( MaxIdeal ` R ) )
5 2 4 syl 
 |-  ( ph -> E. n n e. ( MaxIdeal ` R ) )
6 simpr 
 |-  ( ( ph /\ n e. ( MaxIdeal ` R ) ) -> n e. ( MaxIdeal ` R ) )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 eqid 
 |-  ( MaxIdeal ` R ) = ( MaxIdeal ` R )
9 2 adantr 
 |-  ( ( ph /\ ( MaxIdeal ` R ) = { { .0. } } ) -> R e. NzRing )
10 simpr 
 |-  ( ( ph /\ ( MaxIdeal ` R ) = { { .0. } } ) -> ( MaxIdeal ` R ) = { { .0. } } )
11 7 1 8 9 10 drngmxidlr 
 |-  ( ( ph /\ ( MaxIdeal ` R ) = { { .0. } } ) -> R e. DivRing )
12 3 11 mtand 
 |-  ( ph -> -. ( MaxIdeal ` R ) = { { .0. } } )
13 12 neqned 
 |-  ( ph -> ( MaxIdeal ` R ) =/= { { .0. } } )
14 13 adantr 
 |-  ( ( ph /\ n e. ( MaxIdeal ` R ) ) -> ( MaxIdeal ` R ) =/= { { .0. } } )
15 n0nsnel 
 |-  ( ( n e. ( MaxIdeal ` R ) /\ ( MaxIdeal ` R ) =/= { { .0. } } ) -> E. m e. ( MaxIdeal ` R ) m =/= { .0. } )
16 6 14 15 syl2anc 
 |-  ( ( ph /\ n e. ( MaxIdeal ` R ) ) -> E. m e. ( MaxIdeal ` R ) m =/= { .0. } )
17 5 16 exlimddv 
 |-  ( ph -> E. m e. ( MaxIdeal ` R ) m =/= { .0. } )