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 Could not format assertion : No typesetting found for |- ( R e. NzRing -> E. m m e. ( MaxIdeal ` R ) ) with typecode |-

Proof

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