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={opp}_r\left(R\right)$$
	oppr2idl.2	$$⊢\phi \to R\in \mathrm{Ring}$$
	opprmxidl.3	No typesetting found for |- ( ph -> M e. ( MaxIdeal ` R ) ) with typecode |-
Assertion	opprmxidlabs	Could not format assertion : No typesetting found for |- ( ph -> M e. ( MaxIdeal ` ( oppR ` O ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oppreqg.o	$$⊢O={opp}_r\left(R\right)$$
2		oppr2idl.2	$$⊢\phi \to R\in \mathrm{Ring}$$
3		opprmxidl.3	Could not format ( ph -> M e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ph -> M e. ( MaxIdeal ` R ) ) with typecode |-
4	1	opprring	$$⊢R\in \mathrm{Ring}\to O\in \mathrm{Ring}$$
5		eqid	$$⊢{opp}_r\left(O\right)={opp}_r\left(O\right)$$
6	5	opprring	$$⊢O\in \mathrm{Ring}\to {opp}_r\left(O\right)\in \mathrm{Ring}$$
7	2 4 6	3syl	$$⊢\phi \to {opp}_r\left(O\right)\in \mathrm{Ring}$$
8		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
9	8	mxidlidl	Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) with typecode |-
10	2 3 9	syl2anc	$$⊢\phi \to M\in \mathrm{LIdeal}\left(R\right)$$
11	1 2	opprlidlabs	$$⊢\phi \to \mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left({opp}_r\left(O\right)\right)$$
12	10 11	eleqtrd	$$⊢\phi \to M\in \mathrm{LIdeal}\left({opp}_r\left(O\right)\right)$$
13	8	mxidlnr	Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= ( Base ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= ( Base ` R ) ) with typecode |-
14	2 3 13	syl2anc	$$⊢\phi \to M\ne {\mathrm{Base}}_R$$
15	2	ad2antrr	$$⊢\left(\left(\phi \wedge j\in \mathrm{LIdeal}\left({opp}_r\left(O\right)\right)\right)\wedge M\subseteq j\right)\to R\in \mathrm{Ring}$$
16	3	ad2antrr	Could not format ( ( ( ph /\ j e. ( LIdeal ` ( oppR ` O ) ) ) /\ M C_ j ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( ( ph /\ j e. ( LIdeal ` ( oppR ` O ) ) ) /\ M C_ j ) -> M e. ( MaxIdeal ` R ) ) with typecode |-
17		simplr	$$⊢\left(\left(\phi \wedge j\in \mathrm{LIdeal}\left({opp}_r\left(O\right)\right)\right)\wedge M\subseteq j\right)\to j\in \mathrm{LIdeal}\left({opp}_r\left(O\right)\right)$$
18	11	ad2antrr	$$⊢\left(\left(\phi \wedge j\in \mathrm{LIdeal}\left({opp}_r\left(O\right)\right)\right)\wedge M\subseteq j\right)\to \mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left({opp}_r\left(O\right)\right)$$
19	17 18	eleqtrrd	$$⊢\left(\left(\phi \wedge j\in \mathrm{LIdeal}\left({opp}_r\left(O\right)\right)\right)\wedge M\subseteq j\right)\to j\in \mathrm{LIdeal}\left(R\right)$$
20		simpr	$$⊢\left(\left(\phi \wedge j\in \mathrm{LIdeal}\left({opp}_r\left(O\right)\right)\right)\wedge M\subseteq j\right)\to M\subseteq j$$
21	8	mxidlmax	Could not format ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( LIdeal ` R ) /\ M C_ j ) ) -> ( j = M \/ j = ( Base ` R ) ) ) : No typesetting found for |- ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( LIdeal ` R ) /\ M C_ j ) ) -> ( j = M \/ j = ( Base ` R ) ) ) with typecode |-
22	15 16 19 20 21	syl22anc	$$⊢\left(\left(\phi \wedge j\in \mathrm{LIdeal}\left({opp}_r\left(O\right)\right)\right)\wedge M\subseteq j\right)\to \left(j=M\vee j={\mathrm{Base}}_R\right)$$
23	22	ex	$$⊢\left(\phi \wedge j\in \mathrm{LIdeal}\left({opp}_r\left(O\right)\right)\right)\to \left(M\subseteq j\to \left(j=M\vee j={\mathrm{Base}}_R\right)\right)$$
24	23	ralrimiva	$$⊢\phi \to \forall j\in \mathrm{LIdeal}\left({opp}_r\left(O\right)\right)\left(M\subseteq j\to \left(j=M\vee j={\mathrm{Base}}_R\right)\right)$$
25	1 8	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_O$$
26	5 25	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{opp}_r\left(O\right)}$$
27	26	ismxidl	Could not format ( ( 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 ) ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) ) with typecode |-
28	27	biimpar	Could not format ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-
29	7 12 14 24 28	syl13anc	Could not format ( ph -> M e. ( MaxIdeal ` ( oppR ` O ) ) ) : No typesetting found for |- ( ph -> M e. ( MaxIdeal ` ( oppR ` O ) ) ) with typecode |-