Theorem 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	⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) )
	qsfld.2	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	qsfld.3	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
	qsfld.4	⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
Assertion	qsfld	⊢ ( 𝜑 → ( 𝑄 ∈ Field ↔ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		qsfld.1	⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) )
2		qsfld.2	⊢ ( 𝜑 → 𝑅 ∈ CRing )
3		qsfld.3	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
4		qsfld.4	⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
5		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
6		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
7	6	crng2idl	⊢ ( 𝑅 ∈ CRing → ( LIdeal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) )
8	2 7	syl	⊢ ( 𝜑 → ( LIdeal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) )
9	4 8	eleqtrd	⊢ ( 𝜑 → 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) )
10	5 1 3 9	qsdrng	⊢ ( 𝜑 → ( 𝑄 ∈ DivRing ↔ ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ 𝑀 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑅 ) ) ) ) )
11		isfld	⊢ ( 𝑄 ∈ Field ↔ ( 𝑄 ∈ DivRing ∧ 𝑄 ∈ CRing ) )
12	1 6	quscrng	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑄 ∈ CRing )
13	2 4 12	syl2anc	⊢ ( 𝜑 → 𝑄 ∈ CRing )
14	13	biantrud	⊢ ( 𝜑 → ( 𝑄 ∈ DivRing ↔ ( 𝑄 ∈ DivRing ∧ 𝑄 ∈ CRing ) ) )
15	11 14	bitr4id	⊢ ( 𝜑 → ( 𝑄 ∈ Field ↔ 𝑄 ∈ DivRing ) )
16		eqid	⊢ ( MaxIdeal ‘ 𝑅 ) = ( MaxIdeal ‘ 𝑅 )
17	16 5	crngmxidl	⊢ ( 𝑅 ∈ CRing → ( MaxIdeal ‘ 𝑅 ) = ( MaxIdeal ‘ ( oppr ‘ 𝑅 ) ) )
18	2 17	syl	⊢ ( 𝜑 → ( MaxIdeal ‘ 𝑅 ) = ( MaxIdeal ‘ ( oppr ‘ 𝑅 ) ) )
19	18	eleq2d	⊢ ( 𝜑 → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ 𝑀 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
20	19	biimpd	⊢ ( 𝜑 → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) → 𝑀 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
21	20	pm4.71d	⊢ ( 𝜑 → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ 𝑀 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑅 ) ) ) ) )
22	10 15 21	3bitr4d	⊢ ( 𝜑 → ( 𝑄 ∈ Field ↔ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) )