Metamath Proof Explorer

Theorem krull

Description: Krull's theorem: Any nonzero ring has at least one maximal ideal. (Contributed by Thierry Arnoux, 10-Apr-2024)

Ref Expression
Assertion krull 
|- ( R e. NzRing -> E. m m e. ( MaxIdeal ` R ) )

Proof

Step Hyp Ref Expression
1 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
2 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
3 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
4 2 3 lidl0 
 |-  ( R e. Ring -> { ( 0g ` R ) } e. ( LIdeal ` R ) )
5 1 4 syl 
 |-  ( R e. NzRing -> { ( 0g ` R ) } e. ( LIdeal ` R ) )
6 fvex 
 |-  ( 0g ` R ) e. _V
7 hashsng 
 |-  ( ( 0g ` R ) e. _V -> ( # ` { ( 0g ` R ) } ) = 1 )
8 6 7 ax-mp 
 |-  ( # ` { ( 0g ` R ) } ) = 1
9 simpr 
 |-  ( ( R e. NzRing /\ { ( 0g ` R ) } = ( Base ` R ) ) -> { ( 0g ` R ) } = ( Base ` R ) )
10 9 fveq2d 
 |-  ( ( R e. NzRing /\ { ( 0g ` R ) } = ( Base ` R ) ) -> ( # ` { ( 0g ` R ) } ) = ( # ` ( Base ` R ) ) )
11 8 10 eqtr3id 
 |-  ( ( R e. NzRing /\ { ( 0g ` R ) } = ( Base ` R ) ) -> 1 = ( # ` ( Base ` R ) ) )
12 1red 
 |-  ( ( R e. NzRing /\ { ( 0g ` R ) } = ( Base ` R ) ) -> 1 e. RR )
13 eqid 
 |-  ( Base ` R ) = ( Base ` R )
14 13 isnzr2hash 
 |-  ( R e. NzRing <-> ( R e. Ring /\ 1 < ( # ` ( Base ` R ) ) ) )
15 14 simprbi 
 |-  ( R e. NzRing -> 1 < ( # ` ( Base ` R ) ) )
16 15 adantr 
 |-  ( ( R e. NzRing /\ { ( 0g ` R ) } = ( Base ` R ) ) -> 1 < ( # ` ( Base ` R ) ) )
17 12 16 ltned 
 |-  ( ( R e. NzRing /\ { ( 0g ` R ) } = ( Base ` R ) ) -> 1 =/= ( # ` ( Base ` R ) ) )
18 17 neneqd 
 |-  ( ( R e. NzRing /\ { ( 0g ` R ) } = ( Base ` R ) ) -> -. 1 = ( # ` ( Base ` R ) ) )
19 11 18 pm2.65da 
 |-  ( R e. NzRing -> -. { ( 0g ` R ) } = ( Base ` R ) )
20 19 neqned 
 |-  ( R e. NzRing -> { ( 0g ` R ) } =/= ( Base ` R ) )
21 13 ssmxidl 
 |-  ( ( R e. Ring /\ { ( 0g ` R ) } e. ( LIdeal ` R ) /\ { ( 0g ` R ) } =/= ( Base ` R ) ) -> E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m )
22 1 5 20 21 syl3anc 
 |-  ( R e. NzRing -> E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m )
23 df-rex 
 |-  ( E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m <-> E. m ( m e. ( MaxIdeal ` R ) /\ { ( 0g ` R ) } C_ m ) )
24 exsimpl 
 |-  ( E. m ( m e. ( MaxIdeal ` R ) /\ { ( 0g ` R ) } C_ m ) -> E. m m e. ( MaxIdeal ` R ) )
25 23 24 sylbi 
 |-  ( E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m -> E. m m e. ( MaxIdeal ` R ) )
26 22 25 syl 
 |-  ( R e. NzRing -> E. m m e. ( MaxIdeal ` R ) )