Metamath Proof Explorer

Theorem ismaxidl

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

Ref Expression
Hypotheses ismaxidl.1 ⊢G=1st⁡R
ismaxidl.2 ⊢X=ran⁡G
Assertion ismaxidl ⊢R∈RingOps→M∈MaxIdl⁡R↔M∈Idl⁡R∧M≠X∧∀j∈Idl⁡RM⊆j→j=M∨j=X

Proof

Step Hyp Ref Expression
1 ismaxidl.1 ⊢G=1st⁡R
2 ismaxidl.2 ⊢X=ran⁡G
3 1 2 maxidlval ⊢R∈RingOps→MaxIdl⁡R=i∈Idl⁡R|i≠X∧∀j∈Idl⁡Ri⊆j→j=i∨j=X
4 3 eleq2d ⊢R∈RingOps→M∈MaxIdl⁡R↔M∈i∈Idl⁡R|i≠X∧∀j∈Idl⁡Ri⊆j→j=i∨j=X
5 neeq1 ⊢i=M→i≠X↔M≠X
6 sseq1 ⊢i=M→i⊆j↔M⊆j
7 eqeq2 ⊢i=M→j=i↔j=M
8 7 orbi1d ⊢i=M→j=i∨j=X↔j=M∨j=X
9 6 8 imbi12d ⊢i=M→i⊆j→j=i∨j=X↔M⊆j→j=M∨j=X
10 9 ralbidv ⊢i=M→∀j∈Idl⁡Ri⊆j→j=i∨j=X↔∀j∈Idl⁡RM⊆j→j=M∨j=X
11 5 10 anbi12d ⊢i=M→i≠X∧∀j∈Idl⁡Ri⊆j→j=i∨j=X↔M≠X∧∀j∈Idl⁡RM⊆j→j=M∨j=X
12 11 elrab ⊢M∈i∈Idl⁡R|i≠X∧∀j∈Idl⁡Ri⊆j→j=i∨j=X↔M∈Idl⁡R∧M≠X∧∀j∈Idl⁡RM⊆j→j=M∨j=X
13 3anass ⊢M∈Idl⁡R∧M≠X∧∀j∈Idl⁡RM⊆j→j=M∨j=X↔M∈Idl⁡R∧M≠X∧∀j∈Idl⁡RM⊆j→j=M∨j=X
14 12 13 bitr4i ⊢M∈i∈Idl⁡R|i≠X∧∀j∈Idl⁡Ri⊆j→j=i∨j=X↔M∈Idl⁡R∧M≠X∧∀j∈Idl⁡RM⊆j→j=M∨j=X
15 4 14 bitrdi ⊢R∈RingOps→M∈MaxIdl⁡R↔M∈Idl⁡R∧M≠X∧∀j∈Idl⁡RM⊆j→j=M∨j=X