Metamath Proof Explorer

Theorem mxidlmax

Description: A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Hypothesis mxidlval.1 
|- B = ( Base ` R )
Assertion mxidlmax 
|- ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ M C_ I ) ) -> ( I = M \/ I = B ) )

Proof

Step Hyp Ref Expression
1 mxidlval.1 
 |-  B = ( Base ` R )
2 sseq2 
 |-  ( j = I -> ( M C_ j <-> M C_ I ) )
3 eqeq1 
 |-  ( j = I -> ( j = M <-> I = M ) )
4 eqeq1 
 |-  ( j = I -> ( j = B <-> I = B ) )
5 3 4 orbi12d 
 |-  ( j = I -> ( ( j = M \/ j = B ) <-> ( I = M \/ I = B ) ) )
6 2 5 imbi12d 
 |-  ( j = I -> ( ( M C_ j -> ( j = M \/ j = B ) ) <-> ( M C_ I -> ( I = M \/ I = B ) ) ) )
7 1 ismxidl 
 |-  ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) ) )
8 7 biimpa 
 |-  ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) )
9 8 simp3d 
 |-  ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) )
10 9 adantr 
 |-  ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ I e. ( LIdeal ` R ) ) -> A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) )
11 simpr 
 |-  ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ I e. ( LIdeal ` R ) ) -> I e. ( LIdeal ` R ) )
12 6 10 11 rspcdva 
 |-  ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ I e. ( LIdeal ` R ) ) -> ( M C_ I -> ( I = M \/ I = B ) ) )
13 12 impr 
 |-  ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ M C_ I ) ) -> ( I = M \/ I = B ) )