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

Metamath Proof Explorer

Theorem mxidlmaxv

Description: An ideal I strictly containing a maximal ideal M is the whole ring B . (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses mxidlmaxv.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
mxidlmaxv.2 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mxidlmaxv.3 ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
mxidlmaxv.4 ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
mxidlmaxv.5 ⊢ ( 𝜑 → 𝑀 ⊆ 𝐼 )
mxidlmaxv.6 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐼 ∖ 𝑀 ) )
Assertion mxidlmaxv ( 𝜑 → 𝐼 = 𝐵 )

Proof

Step Hyp Ref Expression
1 mxidlmaxv.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 mxidlmaxv.2 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
3 mxidlmaxv.3 ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
4 mxidlmaxv.4 ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
5 mxidlmaxv.5 ⊢ ( 𝜑 → 𝑀 ⊆ 𝐼 )
6 mxidlmaxv.6 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐼 ∖ 𝑀 ) )
7 1 mxidlmax ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ⊆ 𝐼 ) ) → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝐵 ) )
8 2 3 4 5 7 syl22anc ⊢ ( 𝜑 → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝐵 ) )
9 6 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
10 6 eldifbd ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑀 )
11 nelne1 ⊢ ( ( 𝑋 ∈ 𝐼 ∧ ¬ 𝑋 ∈ 𝑀 ) → 𝐼 ≠ 𝑀 )
12 9 10 11 syl2anc ⊢ ( 𝜑 → 𝐼 ≠ 𝑀 )
13 12 neneqd ⊢ ( 𝜑 → ¬ 𝐼 = 𝑀 )
14 8 13 orcnd ⊢ ( 𝜑 → 𝐼 = 𝐵 )