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 ( 𝑅 ∈ NzRing → ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 nzrring ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
2 eqid ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
3 eqid ( 0g𝑅 ) = ( 0g𝑅 )
4 2 3 lidl0 ( 𝑅 ∈ Ring → { ( 0g𝑅 ) } ∈ ( LIdeal ‘ 𝑅 ) )
5 1 4 syl ( 𝑅 ∈ NzRing → { ( 0g𝑅 ) } ∈ ( LIdeal ‘ 𝑅 ) )
6 fvex ( 0g𝑅 ) ∈ V
7 hashsng ( ( 0g𝑅 ) ∈ V → ( ♯ ‘ { ( 0g𝑅 ) } ) = 1 )
8 6 7 ax-mp ( ♯ ‘ { ( 0g𝑅 ) } ) = 1
9 simpr ( ( 𝑅 ∈ NzRing ∧ { ( 0g𝑅 ) } = ( Base ‘ 𝑅 ) ) → { ( 0g𝑅 ) } = ( Base ‘ 𝑅 ) )
10 9 fveq2d ( ( 𝑅 ∈ NzRing ∧ { ( 0g𝑅 ) } = ( Base ‘ 𝑅 ) ) → ( ♯ ‘ { ( 0g𝑅 ) } ) = ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
11 8 10 eqtr3id ( ( 𝑅 ∈ NzRing ∧ { ( 0g𝑅 ) } = ( Base ‘ 𝑅 ) ) → 1 = ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
12 1red ( ( 𝑅 ∈ NzRing ∧ { ( 0g𝑅 ) } = ( Base ‘ 𝑅 ) ) → 1 ∈ ℝ )
13 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 13 isnzr2hash ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) )
15 14 simprbi ( 𝑅 ∈ NzRing → 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
16 15 adantr ( ( 𝑅 ∈ NzRing ∧ { ( 0g𝑅 ) } = ( Base ‘ 𝑅 ) ) → 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
17 12 16 ltned ( ( 𝑅 ∈ NzRing ∧ { ( 0g𝑅 ) } = ( Base ‘ 𝑅 ) ) → 1 ≠ ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
18 17 neneqd ( ( 𝑅 ∈ NzRing ∧ { ( 0g𝑅 ) } = ( Base ‘ 𝑅 ) ) → ¬ 1 = ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
19 11 18 pm2.65da ( 𝑅 ∈ NzRing → ¬ { ( 0g𝑅 ) } = ( Base ‘ 𝑅 ) )
20 19 neqned ( 𝑅 ∈ NzRing → { ( 0g𝑅 ) } ≠ ( Base ‘ 𝑅 ) )
21 13 ssmxidl ( ( 𝑅 ∈ Ring ∧ { ( 0g𝑅 ) } ∈ ( LIdeal ‘ 𝑅 ) ∧ { ( 0g𝑅 ) } ≠ ( Base ‘ 𝑅 ) ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) { ( 0g𝑅 ) } ⊆ 𝑚 )
22 1 5 20 21 syl3anc ( 𝑅 ∈ NzRing → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) { ( 0g𝑅 ) } ⊆ 𝑚 )
23 df-rex ( ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) { ( 0g𝑅 ) } ⊆ 𝑚 ↔ ∃ 𝑚 ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ { ( 0g𝑅 ) } ⊆ 𝑚 ) )
24 exsimpl ( ∃ 𝑚 ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ { ( 0g𝑅 ) } ⊆ 𝑚 ) → ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
25 23 24 sylbi ( ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) { ( 0g𝑅 ) } ⊆ 𝑚 → ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
26 22 25 syl ( 𝑅 ∈ NzRing → ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )