Metamath Proof Explorer

Theorem opprmxidlabs

Description: The maximal ideal of the opposite ring's opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses oppreqg.o 
|- O = ( oppR ` R )
oppr2idl.2 
|- ( ph -> R e. Ring )
opprmxidl.3 
|- ( ph -> M e. ( MaxIdeal ` R ) )
Assertion opprmxidlabs 
|- ( ph -> M e. ( MaxIdeal ` ( oppR ` O ) ) )

Proof

Step Hyp Ref Expression
1 oppreqg.o 
 |-  O = ( oppR ` R )
2 oppr2idl.2 
 |-  ( ph -> R e. Ring )
3 opprmxidl.3 
 |-  ( ph -> M e. ( MaxIdeal ` R ) )
4 1 opprring 
 |-  ( R e. Ring -> O e. Ring )
5 eqid 
 |-  ( oppR ` O ) = ( oppR ` O )
6 5 opprring 
 |-  ( O e. Ring -> ( oppR ` O ) e. Ring )
7 2 4 6 3syl 
 |-  ( ph -> ( oppR ` O ) e. Ring )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 8 mxidlidl 
 |-  ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) )
10 2 3 9 syl2anc 
 |-  ( ph -> M e. ( LIdeal ` R ) )
11 1 2 opprlidlabs 
 |-  ( ph -> ( LIdeal ` R ) = ( LIdeal ` ( oppR ` O ) ) )
12 10 11 eleqtrd 
 |-  ( ph -> M e. ( LIdeal ` ( oppR ` O ) ) )
13 8 mxidlnr 
 |-  ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= ( Base ` R ) )
14 2 3 13 syl2anc 
 |-  ( ph -> M =/= ( Base ` R ) )
15 2 ad2antrr 
 |-  ( ( ( ph /\ j e. ( LIdeal ` ( oppR ` O ) ) ) /\ M C_ j ) -> R e. Ring )
16 3 ad2antrr 
 |-  ( ( ( ph /\ j e. ( LIdeal ` ( oppR ` O ) ) ) /\ M C_ j ) -> M e. ( MaxIdeal ` R ) )
17 simplr 
 |-  ( ( ( ph /\ j e. ( LIdeal ` ( oppR ` O ) ) ) /\ M C_ j ) -> j e. ( LIdeal ` ( oppR ` O ) ) )
18 11 ad2antrr 
 |-  ( ( ( ph /\ j e. ( LIdeal ` ( oppR ` O ) ) ) /\ M C_ j ) -> ( LIdeal ` R ) = ( LIdeal ` ( oppR ` O ) ) )
19 17 18 eleqtrrd 
 |-  ( ( ( ph /\ j e. ( LIdeal ` ( oppR ` O ) ) ) /\ M C_ j ) -> j e. ( LIdeal ` R ) )
20 simpr 
 |-  ( ( ( ph /\ j e. ( LIdeal ` ( oppR ` O ) ) ) /\ M C_ j ) -> M C_ j )
21 8 mxidlmax 
 |-  ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( LIdeal ` R ) /\ M C_ j ) ) -> ( j = M \/ j = ( Base ` R ) ) )
22 15 16 19 20 21 syl22anc 
 |-  ( ( ( ph /\ j e. ( LIdeal ` ( oppR ` O ) ) ) /\ M C_ j ) -> ( j = M \/ j = ( Base ` R ) ) )
23 22 ex 
 |-  ( ( ph /\ j e. ( LIdeal ` ( oppR ` O ) ) ) -> ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) )
24 23 ralrimiva 
 |-  ( ph -> A. j e. ( LIdeal ` ( oppR ` O ) ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) )
25 1 8 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
26 5 25 opprbas 
 |-  ( Base ` R ) = ( Base ` ( oppR ` O ) )
27 26 ismxidl 
 |-  ( ( oppR ` O ) e. Ring -> ( M e. ( MaxIdeal ` ( oppR ` O ) ) <-> ( M e. ( LIdeal ` ( oppR ` O ) ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` ( oppR ` O ) ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) )
28 27 biimpar 
 |-  ( ( ( oppR ` O ) e. Ring /\ ( M e. ( LIdeal ` ( oppR ` O ) ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` ( oppR ` O ) ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) -> M e. ( MaxIdeal ` ( oppR ` O ) ) )
29 7 12 14 24 28 syl13anc 
 |-  ( ph -> M e. ( MaxIdeal ` ( oppR ` O ) ) )