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 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
mxidlprmALT.2 ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
Assertion mxidlprmALT ( 𝜑 → 𝑀 ∈ ( PrmIdeal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 mxidlprmALT.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
2 mxidlprmALT.2 ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
3 eqid ⊢ ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) ) = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) )
4 1 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 5 mxidlnzr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑅 ∈ NzRing )
7 4 2 6 syl2anc ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
8 5 mxidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
9 4 2 8 syl2anc ⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
10 3 1 7 9 qsfld ⊢ ( 𝜑 → ( ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) ) ∈ Field ↔ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) )
11 2 10 mpbird ⊢ ( 𝜑 → ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) ) ∈ Field )
12 fldidom ⊢ ( ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) ) ∈ Field → ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) ) ∈ IDomn )
13 11 12 syl ⊢ ( 𝜑 → ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) ) ∈ IDomn )
14 3 qsidom ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) ) ∈ IDomn ↔ 𝑀 ∈ ( PrmIdeal ‘ 𝑅 ) ) )
15 1 9 14 syl2anc ⊢ ( 𝜑 → ( ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) ) ∈ IDomn ↔ 𝑀 ∈ ( PrmIdeal ‘ 𝑅 ) ) )
16 13 15 mpbid ⊢ ( 𝜑 → 𝑀 ∈ ( PrmIdeal ‘ 𝑅 ) )