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 ⊢1st⁡R=1st⁡R
2 eqid ⊢ran⁡1st⁡R=ran⁡1st⁡R
3 1 2 ismaxidl ⊢R∈RingOps→M∈MaxIdl⁡R↔M∈Idl⁡R∧M≠ran⁡1st⁡R∧∀j∈Idl⁡RM⊆j→j=M∨j=ran⁡1st⁡R
4 3anass ⊢M∈Idl⁡R∧M≠ran⁡1st⁡R∧∀j∈Idl⁡RM⊆j→j=M∨j=ran⁡1st⁡R↔M∈Idl⁡R∧M≠ran⁡1st⁡R∧∀j∈Idl⁡RM⊆j→j=M∨j=ran⁡1st⁡R
5 3 4 bitrdi ⊢R∈RingOps→M∈MaxIdl⁡R↔M∈Idl⁡R∧M≠ran⁡1st⁡R∧∀j∈Idl⁡RM⊆j→j=M∨j=ran⁡1st⁡R
6 5 simprbda ⊢R∈RingOps∧M∈MaxIdl⁡R→M∈Idl⁡R