This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑅 ) )