Metamath Proof Explorer


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 / 𝑠 R ~ QG M
qsfld.2 φ R CRing
qsfld.3 φ R NzRing
qsfld.4 φ M LIdeal R
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 / 𝑠 R ~ QG M
2 qsfld.2 φ R CRing
3 qsfld.3 φ R NzRing
4 qsfld.4 φ M LIdeal R
5 eqid opp r R = opp r R
6 eqid LIdeal R = LIdeal R
7 6 crng2idl R CRing LIdeal R = 2Ideal R
8 2 7 syl φ LIdeal R = 2Ideal R
9 4 8 eleqtrd φ M 2Ideal R
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 Field Q DivRing Q CRing
12 1 6 quscrng R CRing M LIdeal R Q CRing
13 2 4 12 syl2anc φ Q CRing
14 13 biantrud φ Q DivRing Q DivRing Q CRing
15 11 14 bitr4id φ Q Field Q DivRing
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 |-