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	|- Q = ( R /s ( R ~QG M ) )
	qsfld.2	|- ( ph -> R e. CRing )
	qsfld.3	|- ( ph -> R e. NzRing )
	qsfld.4	|- ( ph -> M e. ( LIdeal ` R ) )
Assertion	qsfld	|- ( ph -> ( Q e. Field <-> M e. ( MaxIdeal ` R ) ) )

Proof

Step	Hyp	Ref	Expression
1		qsfld.1	|- Q = ( R /s ( R ~QG M ) )
2		qsfld.2	|- ( ph -> R e. CRing )
3		qsfld.3	|- ( ph -> R e. NzRing )
4		qsfld.4	|- ( ph -> M e. ( LIdeal ` R ) )
5		eqid	|- ( oppR ` R ) = ( oppR ` R )
6		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
7	6	crng2idl	|- ( R e. CRing -> ( LIdeal ` R ) = ( 2Ideal ` R ) )
8	2 7	syl	|- ( ph -> ( LIdeal ` R ) = ( 2Ideal ` R ) )
9	4 8	eleqtrd	|- ( ph -> M e. ( 2Ideal ` R ) )
10	5 1 3 9	qsdrng	|- ( ph -> ( Q e. DivRing <-> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` ( oppR ` R ) ) ) ) )
11		isfld	|- ( Q e. Field <-> ( Q e. DivRing /\ Q e. CRing ) )
12	1 6	quscrng	|- ( ( R e. CRing /\ M e. ( LIdeal ` R ) ) -> Q e. CRing )
13	2 4 12	syl2anc	|- ( ph -> Q e. CRing )
14	13	biantrud	|- ( ph -> ( Q e. DivRing <-> ( Q e. DivRing /\ Q e. CRing ) ) )
15	11 14	bitr4id	|- ( ph -> ( Q e. Field <-> Q e. DivRing ) )
16		eqid	|- ( MaxIdeal ` R ) = ( MaxIdeal ` R )
17	16 5	crngmxidl	|- ( R e. CRing -> ( MaxIdeal ` R ) = ( MaxIdeal ` ( oppR ` R ) ) )
18	2 17	syl	|- ( ph -> ( MaxIdeal ` R ) = ( MaxIdeal ` ( oppR ` R ) ) )
19	18	eleq2d	|- ( ph -> ( M e. ( MaxIdeal ` R ) <-> M e. ( MaxIdeal ` ( oppR ` R ) ) ) )
20	19	biimpd	|- ( ph -> ( M e. ( MaxIdeal ` R ) -> M e. ( MaxIdeal ` ( oppR ` R ) ) ) )
21	20	pm4.71d	|- ( ph -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` ( oppR ` R ) ) ) ) )
22	10 15 21	3bitr4d	|- ( ph -> ( Q e. Field <-> M e. ( MaxIdeal ` R ) ) )