Metamath Proof Explorer


Theorem mxidlidl

Description: A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Hypothesis mxidlval.1 𝐵 = ( Base ‘ 𝑅 )
Assertion mxidlidl ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 mxidlval.1 𝐵 = ( Base ‘ 𝑅 )
2 1 ismxidl ( 𝑅 ∈ Ring → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀𝑗 → ( 𝑗 = 𝑀𝑗 = 𝐵 ) ) ) ) )
3 2 biimpa ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀𝑗 → ( 𝑗 = 𝑀𝑗 = 𝐵 ) ) ) )
4 3 simp1d ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )