Metamath Proof Explorer

Theorem maxidlmax

Description: A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Hypotheses maxidlnr.1 ⊢G=1st⁡R
maxidlnr.2 ⊢X=ran⁡G
Assertion maxidlmax ⊢R∈RingOps∧M∈MaxIdl⁡R∧I∈Idl⁡R∧M⊆I→I=M∨I=X

Proof

Step Hyp Ref Expression
1 maxidlnr.1 ⊢G=1st⁡R
2 maxidlnr.2 ⊢X=ran⁡G
3 1 2 ismaxidl ⊢R∈RingOps→M∈MaxIdl⁡R↔M∈Idl⁡R∧M≠X∧∀j∈Idl⁡RM⊆j→j=M∨j=X
4 3 biimpa ⊢R∈RingOps∧M∈MaxIdl⁡R→M∈Idl⁡R∧M≠X∧∀j∈Idl⁡RM⊆j→j=M∨j=X
5 4 simp3d ⊢R∈RingOps∧M∈MaxIdl⁡R→∀j∈Idl⁡RM⊆j→j=M∨j=X
6 sseq2 ⊢j=I→M⊆j↔M⊆I
7 eqeq1 ⊢j=I→j=M↔I=M
8 eqeq1 ⊢j=I→j=X↔I=X
9 7 8 orbi12d ⊢j=I→j=M∨j=X↔I=M∨I=X
10 6 9 imbi12d ⊢j=I→M⊆j→j=M∨j=X↔M⊆I→I=M∨I=X
11 10 rspcva ⊢I∈Idl⁡R∧∀j∈Idl⁡RM⊆j→j=M∨j=X→M⊆I→I=M∨I=X
12 5 11 sylan2 ⊢I∈Idl⁡R∧R∈RingOps∧M∈MaxIdl⁡R→M⊆I→I=M∨I=X
13 12 ancoms ⊢R∈RingOps∧M∈MaxIdl⁡R∧I∈Idl⁡R→M⊆I→I=M∨I=X
14 13 impr ⊢R∈RingOps∧M∈MaxIdl⁡R∧I∈Idl⁡R∧M⊆I→I=M∨I=X