qsfld

Description: An ideal M in the commutative ring R is maximal if and only if the factor ring Q is a field. (Contributed by Thierry Arnoux, 13-Mar-2025)

	Ref	Expression
Hypotheses	qsfld.1	$⊢ Q = R /_{𝑠} (R ~_{QG} M)$
	qsfld.2	$⊢ φ \to R \in CRing$
	qsfld.3	$⊢ φ \to R \in NzRing$
	qsfld.4	$⊢ φ \to M \in LIdeal (R)$
Assertion	qsfld	$⊢ φ \to (Q \in Field \leftrightarrow M \in MaxIdeal (R))$

Proof

Step	Hyp	Ref	Expression
1		qsfld.1	$⊢ Q = R /_{𝑠} (R ~_{QG} M)$
2		qsfld.2	$⊢ φ \to R \in CRing$
3		qsfld.3	$⊢ φ \to R \in NzRing$
4		qsfld.4	$⊢ φ \to M \in LIdeal (R)$
5		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
6		eqid	$⊢ LIdeal (R) = LIdeal (R)$
7	6	crng2idl	$⊢ R \in CRing \to LIdeal (R) = 2Ideal (R)$
8	2 7	syl	$⊢ φ \to LIdeal (R) = 2Ideal (R)$
9	4 8	eleqtrd	$⊢ φ \to M \in 2Ideal (R)$
10	5 1 3 9	qsdrng	$⊢ φ \to (Q \in DivRing \leftrightarrow (M \in MaxIdeal (R) \land M \in MaxIdeal ({opp}_{r} (R))))$
11		isfld	$⊢ Q \in Field \leftrightarrow (Q \in DivRing \land Q \in CRing)$
12	1 6	quscrng	$⊢ (R \in CRing \land M \in LIdeal (R)) \to Q \in CRing$
13	2 4 12	syl2anc	$⊢ φ \to Q \in CRing$
14	13	biantrud	$⊢ φ \to (Q \in DivRing \leftrightarrow (Q \in DivRing \land Q \in CRing))$
15	11 14	bitr4id	$⊢ φ \to (Q \in Field \leftrightarrow Q \in DivRing)$
16		eqid	$⊢ MaxIdeal (R) = MaxIdeal (R)$
17	16 5	crngmxidl	$⊢ R \in CRing \to MaxIdeal (R) = MaxIdeal ({opp}_{r} (R))$
18	2 17	syl	$⊢ φ \to MaxIdeal (R) = MaxIdeal ({opp}_{r} (R))$
19	18	eleq2d	$⊢ φ \to (M \in MaxIdeal (R) \leftrightarrow M \in MaxIdeal ({opp}_{r} (R)))$
20	19	biimpd	$⊢ φ \to (M \in MaxIdeal (R) \to M \in MaxIdeal ({opp}_{r} (R)))$
21	20	pm4.71d	$⊢ φ \to (M \in MaxIdeal (R) \leftrightarrow (M \in MaxIdeal (R) \land M \in MaxIdeal ({opp}_{r} (R))))$
22	10 15 21	3bitr4d	$⊢ φ \to (Q \in Field \leftrightarrow M \in MaxIdeal (R))$

Metamath Proof Explorer

Theorem qsfld

Proof