mxidln1

Description: One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

	Ref	Expression
Hypotheses	mxidlval.1	$⊢ B = {Base}_{R}$
	mxidln1.1	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	mxidln1	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to \neg \underset{˙}{1} \in M$

Step	Hyp	Ref	Expression
1		mxidlval.1	$⊢ B = {Base}_{R}$
2		mxidln1.1	$⊢ \underset{˙}{1} = 1_{R}$
3	1	mxidlnr	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to M \neq B$
4	1	mxidlidl	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to M \in LIdeal (R)$
5		eqid	$⊢ LIdeal (R) = LIdeal (R)$
6	5 1 2	lidl1el	$⊢ (R \in Ring \land M \in LIdeal (R)) \to (\underset{˙}{1} \in M \leftrightarrow M = B)$
7	4 6	syldan	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to (\underset{˙}{1} \in M \leftrightarrow M = B)$
8	7	necon3bbid	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to (\neg \underset{˙}{1} \in M \leftrightarrow M \neq B)$
9	3 8	mpbird	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to \neg \underset{˙}{1} \in M$

Metamath Proof Explorer