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

Metamath Proof Explorer

Theorem mxidlprmALT

Description: Every maximal ideal is prime - alternative proof. (Contributed by Thierry Arnoux, 15-Mar-2025) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	mxidlprmALT.1	$⊢ φ \to R \in CRing$
		mxidlprmALT.2	$⊢ φ \to M \in MaxIdeal (R)$
	Assertion	mxidlprmALT	$⊢ φ \to M \in PrmIdeal (R)$

Proof

Step	Hyp	Ref	Expression
1		mxidlprmALT.1	$⊢ φ \to R \in CRing$
2		mxidlprmALT.2	$⊢ φ \to M \in MaxIdeal (R)$
3		eqid	$⊢ R /_{𝑠} (R ~_{QG} M) = R /_{𝑠} (R ~_{QG} M)$
4	1	crngringd	$⊢ φ \to R \in Ring$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	5	mxidlnzr	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to R \in NzRing$
7	4 2 6	syl2anc	$⊢ φ \to R \in NzRing$
8	5	mxidlidl	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to M \in LIdeal (R)$
9	4 2 8	syl2anc	$⊢ φ \to M \in LIdeal (R)$
10	3 1 7 9	qsfld	$⊢ φ \to (R /_{𝑠} (R ~_{QG} M) \in Field \leftrightarrow M \in MaxIdeal (R))$
11	2 10	mpbird	$⊢ φ \to R /_{𝑠} (R ~_{QG} M) \in Field$
12		fldidom	$⊢ R /_{𝑠} (R ~_{QG} M) \in Field \to R /_{𝑠} (R ~_{QG} M) \in IDomn$
13	11 12	syl	$⊢ φ \to R /_{𝑠} (R ~_{QG} M) \in IDomn$
14	3	qsidom	$⊢ (R \in CRing \land M \in LIdeal (R)) \to (R /_{𝑠} (R ~_{QG} M) \in IDomn \leftrightarrow M \in PrmIdeal (R))$
15	1 9 14	syl2anc	$⊢ φ \to (R /_{𝑠} (R ~_{QG} M) \in IDomn \leftrightarrow M \in PrmIdeal (R))$
16	13 15	mpbid	$⊢ φ \to M \in PrmIdeal (R)$