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 ⊢ B = Base R
mxidlmaxv.2 ⊢ φ → R ∈ Ring
mxidlmaxv.3 ⊢ φ → M ∈ MaxIdeal ⁡ R
mxidlmaxv.4 ⊢ φ → I ∈ LIdeal ⁡ R
mxidlmaxv.5 ⊢ φ → M ⊆ I
mxidlmaxv.6 ⊢ φ → X ∈ I ∖ M
Assertion mxidlmaxv ⊢ φ → I = B

Proof

Step Hyp Ref Expression
1 mxidlmaxv.1 ⊢ B = Base R
2 mxidlmaxv.2 ⊢ φ → R ∈ Ring
3 mxidlmaxv.3 ⊢ φ → M ∈ MaxIdeal ⁡ R
4 mxidlmaxv.4 ⊢ φ → I ∈ LIdeal ⁡ R
5 mxidlmaxv.5 ⊢ φ → M ⊆ I
6 mxidlmaxv.6 ⊢ φ → X ∈ I ∖ M
7 1 mxidlmax ⊢ R ∈ Ring ∧ M ∈ MaxIdeal ⁡ R ∧ I ∈ LIdeal ⁡ R ∧ M ⊆ I → I = M ∨ I = B
8 2 3 4 5 7 syl22anc ⊢ φ → I = M ∨ I = B
9 6 eldifad ⊢ φ → X ∈ I
10 6 eldifbd ⊢ φ → ¬ X ∈ M
11 nelne1 ⊢ X ∈ I ∧ ¬ X ∈ M → I ≠ M
12 9 10 11 syl2anc ⊢ φ → I ≠ M
13 12 neneqd ⊢ φ → ¬ I = M
14 8 13 orcnd ⊢ φ → I = B