Theorem 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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mxidln1.1	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	mxidln1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ¬ 1 ∈ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		mxidlval.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		mxidln1.1	⊢ 1 = ( 1r ‘ 𝑅 )
3	1	mxidlnr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ≠ 𝐵 )
4	1	mxidlidl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
5		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
6	5 1 2	lidl1el	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 1 ∈ 𝑀 ↔ 𝑀 = 𝐵 ) )
7	4 6	syldan	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( 1 ∈ 𝑀 ↔ 𝑀 = 𝐵 ) )
8	7	necon3bbid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( ¬ 1 ∈ 𝑀 ↔ 𝑀 ≠ 𝐵 ) )
9	3 8	mpbird	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ¬ 1 ∈ 𝑀 )