This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ 𝑀 )