Theorem mxidlmaxv

Description: An ideal I strictly containing a maximal ideal M is the whole ring B . (Contributed by Thierry Arnoux, 9-Mar-2025)

	Ref	Expression
Hypotheses	mxidlmaxv.1	$$⊢B={\mathrm{Base}}_R$$
	mxidlmaxv.2	$$⊢\phi \to R\in \mathrm{Ring}$$
	mxidlmaxv.3	No typesetting found for |- ( ph -> M e. ( MaxIdeal ` R ) ) with typecode |-
	mxidlmaxv.4	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$
	mxidlmaxv.5	$$⊢\phi \to M\subseteq I$$
	mxidlmaxv.6	$$⊢\phi \to X\in \left(I\setminus M\right)$$
Assertion	mxidlmaxv	$$⊢\phi \to I=B$$

Proof

Step	Hyp	Ref	Expression
1		mxidlmaxv.1	$$⊢B={\mathrm{Base}}_R$$
2		mxidlmaxv.2	$$⊢\phi \to R\in \mathrm{Ring}$$
3		mxidlmaxv.3	Could not format ( ph -> M e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ph -> M e. ( MaxIdeal ` R ) ) with typecode |-
4		mxidlmaxv.4	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$
5		mxidlmaxv.5	$$⊢\phi \to M\subseteq I$$
6		mxidlmaxv.6	$$⊢\phi \to X\in \left(I\setminus M\right)$$
7	1	mxidlmax	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 |-
8	2 3 4 5 7	syl22anc	$$⊢\phi \to \left(I=M\vee I=B\right)$$
9	6	eldifad	$$⊢\phi \to X\in I$$
10	6	eldifbd	$$⊢\phi \to \neg X\in M$$
11		nelne1	$$⊢\left(X\in I\wedge \neg X\in M\right)\to I\ne M$$
12	9 10 11	syl2anc	$$⊢\phi \to I\ne M$$
13	12	neneqd	$$⊢\phi \to \neg I=M$$
14	8 13	orcnd	$$⊢\phi \to I=B$$