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 ) ) )

Metamath Proof Explorer

Theorem qsfld

Proof