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