This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem crngmxidl

Description: In a commutative ring, maximal ideals of the opposite ring coincide with maximal ideals. (Contributed by Thierry Arnoux, 13-Mar-2025)

Ref Expression
Hypotheses crngmxidl.i 
|- M = ( MaxIdeal ` R )
crngmxidl.o 
|- O = ( oppR ` R )
Assertion crngmxidl 
|- ( R e. CRing -> M = ( MaxIdeal ` O ) )

Proof

Step Hyp Ref Expression
1 crngmxidl.i 
 |-  M = ( MaxIdeal ` R )
2 crngmxidl.o 
 |-  O = ( oppR ` R )
3 1 eleq2i 
 |-  ( m e. M <-> m e. ( MaxIdeal ` R ) )
4 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
5 4 2 crngridl 
 |-  ( R e. CRing -> ( LIdeal ` R ) = ( LIdeal ` O ) )
6 5 eleq2d 
 |-  ( R e. CRing -> ( m e. ( LIdeal ` R ) <-> m e. ( LIdeal ` O ) ) )
7 5 raleqdv 
 |-  ( R e. CRing -> ( A. j e. ( LIdeal ` R ) ( m C_ j -> ( j = m \/ j = ( Base ` R ) ) ) <-> A. j e. ( LIdeal ` O ) ( m C_ j -> ( j = m \/ j = ( Base ` R ) ) ) ) )
8 6 7 3anbi13d 
 |-  ( R e. CRing -> ( ( m e. ( LIdeal ` R ) /\ m =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( m C_ j -> ( j = m \/ j = ( Base ` R ) ) ) ) <-> ( m e. ( LIdeal ` O ) /\ m =/= ( Base ` R ) /\ A. j e. ( LIdeal ` O ) ( m C_ j -> ( j = m \/ j = ( Base ` R ) ) ) ) ) )
9 crngring 
 |-  ( R e. CRing -> R e. Ring )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 10 ismxidl 
 |-  ( R e. Ring -> ( m e. ( MaxIdeal ` R ) <-> ( m e. ( LIdeal ` R ) /\ m =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( m C_ j -> ( j = m \/ j = ( Base ` R ) ) ) ) ) )
12 9 11 syl 
 |-  ( R e. CRing -> ( m e. ( MaxIdeal ` R ) <-> ( m e. ( LIdeal ` R ) /\ m =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( m C_ j -> ( j = m \/ j = ( Base ` R ) ) ) ) ) )
13 2 opprring 
 |-  ( R e. Ring -> O e. Ring )
14 2 10 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
15 14 ismxidl 
 |-  ( O e. Ring -> ( m e. ( MaxIdeal ` O ) <-> ( m e. ( LIdeal ` O ) /\ m =/= ( Base ` R ) /\ A. j e. ( LIdeal ` O ) ( m C_ j -> ( j = m \/ j = ( Base ` R ) ) ) ) ) )
16 9 13 15 3syl 
 |-  ( R e. CRing -> ( m e. ( MaxIdeal ` O ) <-> ( m e. ( LIdeal ` O ) /\ m =/= ( Base ` R ) /\ A. j e. ( LIdeal ` O ) ( m C_ j -> ( j = m \/ j = ( Base ` R ) ) ) ) ) )
17 8 12 16 3bitr4d 
 |-  ( R e. CRing -> ( m e. ( MaxIdeal ` R ) <-> m e. ( MaxIdeal ` O ) ) )
18 3 17 bitrid 
 |-  ( R e. CRing -> ( m e. M <-> m e. ( MaxIdeal ` O ) ) )
19 18 eqrdv 
 |-  ( R e. CRing -> M = ( MaxIdeal ` O ) )