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	$⊢ \underset{˙}{0} = 0_{R}$
	krullndrng.2	$⊢ φ \to R \in NzRing$
	krullndrng.3	$⊢ φ \to \neg R \in DivRing$
Assertion	krullndrng	$⊢ φ \to \exists m \in MaxIdeal (R) m \neq \{\underset{˙}{0}\}$

Step	Hyp	Ref	Expression
1		krullndrng.1	$⊢ \underset{˙}{0} = 0_{R}$
2		krullndrng.2	$⊢ φ \to R \in NzRing$
3		krullndrng.3	$⊢ φ \to \neg R \in DivRing$
4		krull	$⊢ R \in NzRing \to \exists n n \in MaxIdeal (R)$
5	2 4	syl	$⊢ φ \to \exists n n \in MaxIdeal (R)$
6		simpr	$⊢ (φ \land n \in MaxIdeal (R)) \to n \in MaxIdeal (R)$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8		eqid	$⊢ MaxIdeal (R) = MaxIdeal (R)$
9	2	adantr	$⊢ (φ \land MaxIdeal (R) = \{\{\underset{˙}{0}\}\}) \to R \in NzRing$
10		simpr	$⊢ (φ \land MaxIdeal (R) = \{\{\underset{˙}{0}\}\}) \to MaxIdeal (R) = \{\{\underset{˙}{0}\}\}$
11	7 1 8 9 10	drngmxidlr	$⊢ (φ \land MaxIdeal (R) = \{\{\underset{˙}{0}\}\}) \to R \in DivRing$
12	3 11	mtand	$⊢ φ \to \neg MaxIdeal (R) = \{\{\underset{˙}{0}\}\}$
13	12	neqned	$⊢ φ \to MaxIdeal (R) \neq \{\{\underset{˙}{0}\}\}$
14	13	adantr	$⊢ (φ \land n \in MaxIdeal (R)) \to MaxIdeal (R) \neq \{\{\underset{˙}{0}\}\}$
15		n0nsnel	$⊢ (n \in MaxIdeal (R) \land MaxIdeal (R) \neq \{\{\underset{˙}{0}\}\}) \to \exists m \in MaxIdeal (R) m \neq \{\underset{˙}{0}\}$
16	6 14 15	syl2anc	$⊢ (φ \land n \in MaxIdeal (R)) \to \exists m \in MaxIdeal (R) m \neq \{\underset{˙}{0}\}$
17	5 16	exlimddv	$⊢ φ \to \exists m \in MaxIdeal (R) m \neq \{\underset{˙}{0}\}$

Metamath Proof Explorer