This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mxidlprmALT

Description: Every maximal ideal is prime - alternative proof. (Contributed by Thierry Arnoux, 15-Mar-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses mxidlprmALT.1 
|- ( ph -> R e. CRing )
mxidlprmALT.2 
|- ( ph -> M e. ( MaxIdeal ` R ) )
Assertion mxidlprmALT 
|- ( ph -> M e. ( PrmIdeal ` R ) )

Proof

Step Hyp Ref Expression
1 mxidlprmALT.1 
 |-  ( ph -> R e. CRing )
2 mxidlprmALT.2 
 |-  ( ph -> M e. ( MaxIdeal ` R ) )
3 eqid 
 |-  ( R /s ( R ~QG M ) ) = ( R /s ( R ~QG M ) )
4 1 crngringd 
 |-  ( ph -> R e. Ring )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 5 mxidlnzr 
 |-  ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> R e. NzRing )
7 4 2 6 syl2anc 
 |-  ( ph -> R e. NzRing )
8 5 mxidlidl 
 |-  ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) )
9 4 2 8 syl2anc 
 |-  ( ph -> M e. ( LIdeal ` R ) )
10 3 1 7 9 qsfld 
 |-  ( ph -> ( ( R /s ( R ~QG M ) ) e. Field <-> M e. ( MaxIdeal ` R ) ) )
11 2 10 mpbird 
 |-  ( ph -> ( R /s ( R ~QG M ) ) e. Field )
12 fldidom 
 |-  ( ( R /s ( R ~QG M ) ) e. Field -> ( R /s ( R ~QG M ) ) e. IDomn )
13 11 12 syl 
 |-  ( ph -> ( R /s ( R ~QG M ) ) e. IDomn )
14 3 qsidom 
 |-  ( ( R e. CRing /\ M e. ( LIdeal ` R ) ) -> ( ( R /s ( R ~QG M ) ) e. IDomn <-> M e. ( PrmIdeal ` R ) ) )
15 1 9 14 syl2anc 
 |-  ( ph -> ( ( R /s ( R ~QG M ) ) e. IDomn <-> M e. ( PrmIdeal ` R ) ) )
16 13 15 mpbid 
 |-  ( ph -> M e. ( PrmIdeal ` R ) )