Metamath Proof Explorer

Theorem ismxidl

Description: The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Hypothesis mxidlval.1 ⊢ B = Base R
Assertion ismxidl ⊢ R ∈ Ring → M ∈ MaxIdeal ⁡ R ↔ M ∈ LIdeal ⁡ R ∧ M ≠ B ∧ ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B

Proof

Step Hyp Ref Expression
1 mxidlval.1 ⊢ B = Base R
2 1 mxidlval ⊢ R ∈ Ring → MaxIdeal ⁡ R = i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ j ∈ LIdeal ⁡ R i ⊆ j → j = i ∨ j = B
3 2 eleq2d ⊢ R ∈ Ring → M ∈ MaxIdeal ⁡ R ↔ M ∈ i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ j ∈ LIdeal ⁡ R i ⊆ j → j = i ∨ j = B
4 neeq1 ⊢ i = M → i ≠ B ↔ M ≠ B
5 sseq1 ⊢ i = M → i ⊆ j ↔ M ⊆ j
6 eqeq2 ⊢ i = M → j = i ↔ j = M
7 6 orbi1d ⊢ i = M → j = i ∨ j = B ↔ j = M ∨ j = B
8 5 7 imbi12d ⊢ i = M → i ⊆ j → j = i ∨ j = B ↔ M ⊆ j → j = M ∨ j = B
9 8 ralbidv ⊢ i = M → ∀ j ∈ LIdeal ⁡ R i ⊆ j → j = i ∨ j = B ↔ ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B
10 4 9 anbi12d ⊢ i = M → i ≠ B ∧ ∀ j ∈ LIdeal ⁡ R i ⊆ j → j = i ∨ j = B ↔ M ≠ B ∧ ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B
11 10 elrab ⊢ M ∈ i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ j ∈ LIdeal ⁡ R i ⊆ j → j = i ∨ j = B ↔ M ∈ LIdeal ⁡ R ∧ M ≠ B ∧ ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B
12 3anass ⊢ M ∈ LIdeal ⁡ R ∧ M ≠ B ∧ ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B ↔ M ∈ LIdeal ⁡ R ∧ M ≠ B ∧ ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B
13 11 12 bitr4i ⊢ M ∈ i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ j ∈ LIdeal ⁡ R i ⊆ j → j = i ∨ j = B ↔ M ∈ LIdeal ⁡ R ∧ M ≠ B ∧ ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B
14 3 13 bitrdi ⊢ R ∈ Ring → M ∈ MaxIdeal ⁡ R ↔ M ∈ LIdeal ⁡ R ∧ M ≠ B ∧ ∀ j ∈ LIdeal ⁡ R M ⊆ j → j = M ∨ j = B