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 RNzRingRRing
2 eqid LIdealR=LIdealR
3 eqid 0R=0R
4 2 3 lidl0 RRing0RLIdealR
5 1 4 syl RNzRing0RLIdealR
6 fvex 0RV
7 hashsng 0RV0R=1
8 6 7 ax-mp 0R=1
9 simpr RNzRing0R=BaseR0R=BaseR
10 9 fveq2d RNzRing0R=BaseR0R=BaseR
11 8 10 eqtr3id RNzRing0R=BaseR1=BaseR
12 1red RNzRing0R=BaseR1
13 eqid BaseR=BaseR
14 13 isnzr2hash RNzRingRRing1<BaseR
15 14 simprbi RNzRing1<BaseR
16 15 adantr RNzRing0R=BaseR1<BaseR
17 12 16 ltned RNzRing0R=BaseR1BaseR
18 17 neneqd RNzRing0R=BaseR¬1=BaseR
19 11 18 pm2.65da RNzRing¬0R=BaseR
20 19 neqned RNzRing0RBaseR
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 |-