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={\mathrm{Base}}_R$$
Assertion	mxidlmax	Could not format assertion : No typesetting found for |- ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ M C_ I ) ) -> ( I = M \/ I = B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mxidlval.1	$$⊢B={\mathrm{Base}}_R$$
2		sseq2	$$⊢j=I\to \left(M\subseteq j\leftrightarrow M\subseteq I\right)$$
3		eqeq1	$$⊢j=I\to \left(j=M\leftrightarrow I=M\right)$$
4		eqeq1	$$⊢j=I\to \left(j=B\leftrightarrow I=B\right)$$
5	3 4	orbi12d	$$⊢j=I\to \left(\left(j=M\vee j=B\right)\leftrightarrow \left(I=M\vee I=B\right)\right)$$
6	2 5	imbi12d	$$⊢j=I\to \left(\left(M\subseteq j\to \left(j=M\vee j=B\right)\right)\leftrightarrow \left(M\subseteq I\to \left(I=M\vee I=B\right)\right)\right)$$
7	1	ismxidl	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
8	7	biimpa	Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
9	8	simp3d	Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) with typecode |-
10	9	adantr	Could not format ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ I e. ( LIdeal ` R ) ) -> A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) : No typesetting found for |- ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ I e. ( LIdeal ` R ) ) -> A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) with typecode |-
11		simpr	Could not format ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ I e. ( LIdeal ` R ) ) -> I e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ I e. ( LIdeal ` R ) ) -> I e. ( LIdeal ` R ) ) with typecode |-
12	6 10 11	rspcdva	Could not format ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ I e. ( LIdeal ` R ) ) -> ( M C_ I -> ( I = M \/ I = B ) ) ) : No typesetting found for |- ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ I e. ( LIdeal ` R ) ) -> ( M C_ I -> ( I = M \/ I = B ) ) ) with typecode |-
13	12	impr	Could not format ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ M C_ I ) ) -> ( I = M \/ I = B ) ) : No typesetting found for |- ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ M C_ I ) ) -> ( I = M \/ I = B ) ) with typecode |-