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{/}_{𝑠}\left(R{~}_{\mathit{QG}}M\right)$$
	qsfld.2	$$⊢\phi \to R\in \mathrm{CRing}$$
	qsfld.3	$$⊢\phi \to R\in \mathrm{NzRing}$$
	qsfld.4	$$⊢\phi \to M\in \mathrm{LIdeal}\left(R\right)$$
Assertion	qsfld	Could not format assertion : No typesetting found for |- ( ph -> ( Q e. Field <-> M e. ( MaxIdeal ` R ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		qsfld.1	$$⊢Q=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}M\right)$$
2		qsfld.2	$$⊢\phi \to R\in \mathrm{CRing}$$
3		qsfld.3	$$⊢\phi \to R\in \mathrm{NzRing}$$
4		qsfld.4	$$⊢\phi \to M\in \mathrm{LIdeal}\left(R\right)$$
5		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
6		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
7	6	crng2idl	$$⊢R\in \mathrm{CRing}\to \mathrm{LIdeal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
8	2 7	syl	$$⊢\phi \to \mathrm{LIdeal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
9	4 8	eleqtrd	$$⊢\phi \to M\in \mathrm{2Ideal}\left(R\right)$$
10	5 1 3 9	qsdrng	Could not format ( ph -> ( Q e. DivRing <-> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` ( oppR ` R ) ) ) ) ) : No typesetting found for |- ( ph -> ( Q e. DivRing <-> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` ( oppR ` R ) ) ) ) ) with typecode |-
11		isfld	$$⊢Q\in \mathrm{Field}\leftrightarrow \left(Q\in \mathrm{DivRing}\wedge Q\in \mathrm{CRing}\right)$$
12	1 6	quscrng	$$⊢\left(R\in \mathrm{CRing}\wedge M\in \mathrm{LIdeal}\left(R\right)\right)\to Q\in \mathrm{CRing}$$
13	2 4 12	syl2anc	$$⊢\phi \to Q\in \mathrm{CRing}$$
14	13	biantrud	$$⊢\phi \to \left(Q\in \mathrm{DivRing}\leftrightarrow \left(Q\in \mathrm{DivRing}\wedge Q\in \mathrm{CRing}\right)\right)$$
15	11 14	bitr4id	$$⊢\phi \to \left(Q\in \mathrm{Field}\leftrightarrow Q\in \mathrm{DivRing}\right)$$
16		eqid	Could not format ( MaxIdeal ` R ) = ( MaxIdeal ` R ) : No typesetting found for |- ( MaxIdeal ` R ) = ( MaxIdeal ` R ) with typecode |-
17	16 5	crngmxidl	Could not format ( R e. CRing -> ( MaxIdeal ` R ) = ( MaxIdeal ` ( oppR ` R ) ) ) : No typesetting found for |- ( R e. CRing -> ( MaxIdeal ` R ) = ( MaxIdeal ` ( oppR ` R ) ) ) with typecode |-
18	2 17	syl	Could not format ( ph -> ( MaxIdeal ` R ) = ( MaxIdeal ` ( oppR ` R ) ) ) : No typesetting found for |- ( ph -> ( MaxIdeal ` R ) = ( MaxIdeal ` ( oppR ` R ) ) ) with typecode |-
19	18	eleq2d	Could not format ( ph -> ( M e. ( MaxIdeal ` R ) <-> M e. ( MaxIdeal ` ( oppR ` R ) ) ) ) : No typesetting found for |- ( ph -> ( M e. ( MaxIdeal ` R ) <-> M e. ( MaxIdeal ` ( oppR ` R ) ) ) ) with typecode |-
20	19	biimpd	Could not format ( ph -> ( M e. ( MaxIdeal ` R ) -> M e. ( MaxIdeal ` ( oppR ` R ) ) ) ) : No typesetting found for |- ( ph -> ( M e. ( MaxIdeal ` R ) -> M e. ( MaxIdeal ` ( oppR ` R ) ) ) ) with typecode |-
21	20	pm4.71d	Could not format ( ph -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` ( oppR ` R ) ) ) ) ) : No typesetting found for |- ( ph -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` ( oppR ` R ) ) ) ) ) with typecode |-
22	10 15 21	3bitr4d	Could not format ( ph -> ( Q e. Field <-> M e. ( MaxIdeal ` R ) ) ) : No typesetting found for |- ( ph -> ( Q e. Field <-> M e. ( MaxIdeal ` R ) ) ) with typecode |-