Metamath Proof Explorer

Theorem maxidlidl

Description: A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011)

Ref Expression
Assertion maxidlidl ⊢ R ∈ RingOps ∧ M ∈ MaxIdl ⁡ R → M ∈ Idl ⁡ R

Proof

Step Hyp Ref Expression
1 eqid ⊢ 1 st ⁡ R = 1 st ⁡ R
2 eqid ⊢ ran ⁡ 1 st ⁡ R = ran ⁡ 1 st ⁡ R
3 1 2 ismaxidl ⊢ R ∈ RingOps → M ∈ MaxIdl ⁡ R ↔ M ∈ Idl ⁡ R ∧ M ≠ ran ⁡ 1 st ⁡ R ∧ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = ran ⁡ 1 st ⁡ R
4 3anass ⊢ M ∈ Idl ⁡ R ∧ M ≠ ran ⁡ 1 st ⁡ R ∧ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = ran ⁡ 1 st ⁡ R ↔ M ∈ Idl ⁡ R ∧ M ≠ ran ⁡ 1 st ⁡ R ∧ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = ran ⁡ 1 st ⁡ R
5 3 4 bitrdi ⊢ R ∈ RingOps → M ∈ MaxIdl ⁡ R ↔ M ∈ Idl ⁡ R ∧ M ≠ ran ⁡ 1 st ⁡ R ∧ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = ran ⁡ 1 st ⁡ R
6 5 simprbda ⊢ R ∈ RingOps ∧ M ∈ MaxIdl ⁡ R → M ∈ Idl ⁡ R