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	No typesetting found for |- M = ( MaxIdeal ` R ) with typecode |-
	crngmxidl.o	$$⊢O={opp}_r\left(R\right)$$
Assertion	crngmxidl	Could not format assertion : No typesetting found for |- ( R e. CRing -> M = ( MaxIdeal ` O ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		crngmxidl.i	Could not format M = ( MaxIdeal ` R ) : No typesetting found for |- M = ( MaxIdeal ` R ) with typecode |-
2		crngmxidl.o	$$⊢O={opp}_r\left(R\right)$$
3	1	eleq2i	Could not format ( m e. M <-> m e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( m e. M <-> m e. ( MaxIdeal ` R ) ) with typecode |-
4		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
5	4 2	crngridl	$$⊢R\in \mathrm{CRing}\to \mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(O\right)$$
6	5	eleq2d	$$⊢R\in \mathrm{CRing}\to \left(m\in \mathrm{LIdeal}\left(R\right)\leftrightarrow m\in \mathrm{LIdeal}\left(O\right)\right)$$
7	5	raleqdv	$$⊢R\in \mathrm{CRing}\to \left(\forall j\in \mathrm{LIdeal}\left(R\right)\left(m\subseteq j\to \left(j=m\vee j={\mathrm{Base}}_R\right)\right)\leftrightarrow \forall j\in \mathrm{LIdeal}\left(O\right)\left(m\subseteq j\to \left(j=m\vee j={\mathrm{Base}}_R\right)\right)\right)$$
8	6 7	3anbi13d	$$⊢R\in \mathrm{CRing}\to \left(\left(m\in \mathrm{LIdeal}\left(R\right)\wedge m\ne {\mathrm{Base}}_R\wedge \forall j\in \mathrm{LIdeal}\left(R\right)\left(m\subseteq j\to \left(j=m\vee j={\mathrm{Base}}_R\right)\right)\right)\leftrightarrow \left(m\in \mathrm{LIdeal}\left(O\right)\wedge m\ne {\mathrm{Base}}_R\wedge \forall j\in \mathrm{LIdeal}\left(O\right)\left(m\subseteq j\to \left(j=m\vee j={\mathrm{Base}}_R\right)\right)\right)\right)$$
9		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
10		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
11	10	ismxidl	Could not format ( 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 ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) with typecode |-
12	9 11	syl	Could not format ( 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 ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) with typecode |-
13	2	opprring	$$⊢R\in \mathrm{Ring}\to O\in \mathrm{Ring}$$
14	2 10	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_O$$
15	14	ismxidl	Could not format ( 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 ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) with typecode |-
16	9 13 15	3syl	Could not format ( 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 ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) with typecode |-
17	8 12 16	3bitr4d	Could not format ( R e. CRing -> ( m e. ( MaxIdeal ` R ) <-> m e. ( MaxIdeal ` O ) ) ) : No typesetting found for |- ( R e. CRing -> ( m e. ( MaxIdeal ` R ) <-> m e. ( MaxIdeal ` O ) ) ) with typecode |-
18	3 17	bitrid	Could not format ( R e. CRing -> ( m e. M <-> m e. ( MaxIdeal ` O ) ) ) : No typesetting found for |- ( R e. CRing -> ( m e. M <-> m e. ( MaxIdeal ` O ) ) ) with typecode |-
19	18	eqrdv	Could not format ( R e. CRing -> M = ( MaxIdeal ` O ) ) : No typesetting found for |- ( R e. CRing -> M = ( MaxIdeal ` O ) ) with typecode |-