Metamath Proof Explorer

Theorem mxidlmax

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

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

Proof

Step Hyp Ref Expression
1 mxidlval.1 ⊢ B = Base R
2 sseq2 ⊢ j = I → M ⊆ j ↔ M ⊆ I
3 eqeq1 ⊢ j = I → j = M ↔ I = M
4 eqeq1 ⊢ j = I → j = B ↔ I = B
5 3 4 orbi12d ⊢ j = I → j = M ∨ j = B ↔ I = M ∨ I = B
6 2 5 imbi12d ⊢ j = I → M ⊆ j → j = M ∨ j = B ↔ M ⊆ I → I = M ∨ I = B
7 1 ismxidl ⊢ R ∈ Ring → M ∈ MaxIdeal ⁡ R ↔ M ∈ LIdeal ⁡ R ∧ M ≠ B ∧ ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B
8 7 biimpa ⊢ R ∈ Ring ∧ M ∈ MaxIdeal ⁡ R → M ∈ LIdeal ⁡ R ∧ M ≠ B ∧ ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B
9 8 simp3d ⊢ R ∈ Ring ∧ M ∈ MaxIdeal ⁡ R → ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B
10 9 adantr ⊢ R ∈ Ring ∧ M ∈ MaxIdeal ⁡ R ∧ I ∈ LIdeal ⁡ R → ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B
11 simpr ⊢ R ∈ Ring ∧ M ∈ MaxIdeal ⁡ R ∧ I ∈ LIdeal ⁡ R → I ∈ LIdeal ⁡ R
12 6 10 11 rspcdva ⊢ R ∈ Ring ∧ M ∈ MaxIdeal ⁡ R ∧ I ∈ LIdeal ⁡ R → M ⊆ I → I = M ∨ I = B
13 12 impr ⊢ R ∈ Ring ∧ M ∈ MaxIdeal ⁡ R ∧ I ∈ LIdeal ⁡ R ∧ M ⊆ I → I = M ∨ I = B