Metamath Proof Explorer

Theorem mxidlnr

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

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

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 simp2d ⊢ R ∈ Ring ∧ M ∈ MaxIdeal ⁡ R → M ≠ B