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

Metamath Proof Explorer

Theorem krullndrng

Description: Krull's theorem for non-division-rings: Existence of a nonzero maximal ideal. (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypotheses krullndrng.1 ⊢ 0 = ( 0g ‘ 𝑅 )
krullndrng.2 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
krullndrng.3 ⊢ ( 𝜑 → ¬ 𝑅 ∈ DivRing )
Assertion krullndrng ( 𝜑 → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) 𝑚 ≠ { 0 } )

Proof

Step Hyp Ref Expression
1 krullndrng.1 ⊢ 0 = ( 0g ‘ 𝑅 )
2 krullndrng.2 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
3 krullndrng.3 ⊢ ( 𝜑 → ¬ 𝑅 ∈ DivRing )
4 krull ⊢ ( 𝑅 ∈ NzRing → ∃ 𝑛 𝑛 ∈ ( MaxIdeal ‘ 𝑅 ) )
5 2 4 syl ⊢ ( 𝜑 → ∃ 𝑛 𝑛 ∈ ( MaxIdeal ‘ 𝑅 ) )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑛 ∈ ( MaxIdeal ‘ 𝑅 ) )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 eqid ⊢ ( MaxIdeal ‘ 𝑅 ) = ( MaxIdeal ‘ 𝑅 )
9 2 adantr ⊢ ( ( 𝜑 ∧ ( MaxIdeal ‘ 𝑅 ) = { { 0 } } ) → 𝑅 ∈ NzRing )
10 simpr ⊢ ( ( 𝜑 ∧ ( MaxIdeal ‘ 𝑅 ) = { { 0 } } ) → ( MaxIdeal ‘ 𝑅 ) = { { 0 } } )
11 7 1 8 9 10 drngmxidlr ⊢ ( ( 𝜑 ∧ ( MaxIdeal ‘ 𝑅 ) = { { 0 } } ) → 𝑅 ∈ DivRing )
12 3 11 mtand ⊢ ( 𝜑 → ¬ ( MaxIdeal ‘ 𝑅 ) = { { 0 } } )
13 12 neqned ⊢ ( 𝜑 → ( MaxIdeal ‘ 𝑅 ) ≠ { { 0 } } )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( MaxIdeal ‘ 𝑅 ) ≠ { { 0 } } )
15 n0nsnel ⊢ ( ( 𝑛 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ ( MaxIdeal ‘ 𝑅 ) ≠ { { 0 } } ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) 𝑚 ≠ { 0 } )
16 6 14 15 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) 𝑚 ≠ { 0 } )
17 5 16 exlimddv ⊢ ( 𝜑 → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) 𝑚 ≠ { 0 } )