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 ∈ NzRing → ∃ m m ∈ MaxIdeal ⁡ R

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 ⊢ R ∈ Ring ∧ 0 R ∈ LIdeal ⁡ R ∧ 0 R ≠ Base R → ∃ m ∈ MaxIdeal ⁡ R 0 R ⊆ m
22 1 5 20 21 syl3anc ⊢ R ∈ NzRing → ∃ m ∈ MaxIdeal ⁡ R 0 R ⊆ m
23 df-rex ⊢ ∃ m ∈ MaxIdeal ⁡ R 0 R ⊆ m ↔ ∃ m m ∈ MaxIdeal ⁡ R ∧ 0 R ⊆ m
24 exsimpl ⊢ ∃ m m ∈ MaxIdeal ⁡ R ∧ 0 R ⊆ m → ∃ m m ∈ MaxIdeal ⁡ R
25 23 24 sylbi ⊢ ∃ m ∈ MaxIdeal ⁡ R 0 R ⊆ m → ∃ m m ∈ MaxIdeal ⁡ R
26 22 25 syl ⊢ R ∈ NzRing → ∃ m m ∈ MaxIdeal ⁡ R