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 } )