Metamath Proof Explorer

Theorem mxidlidl

Description: A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Hypothesis mxidlval.1 ⊢ B = Base R
Assertion mxidlidl ⊢ R ∈ Ring ∧ M ∈ MaxIdeal ⁡ R → M ∈ LIdeal ⁡ R

Proof

Step Hyp Ref Expression
1 mxidlval.1 ⊢ B = Base R
2 1 ismxidl ⊢ R ∈ Ring → M ∈ MaxIdeal ⁡ R ↔ M ∈ LIdeal ⁡ R ∧ M ≠ B ∧ ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B
3 2 biimpa ⊢ R ∈ Ring ∧ M ∈ MaxIdeal ⁡ R → M ∈ LIdeal ⁡ R ∧ M ≠ B ∧ ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B
4 3 simp1d ⊢ R ∈ Ring ∧ M ∈ MaxIdeal ⁡ R → M ∈ LIdeal ⁡ R