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 ‘ 𝑅 ) ) |
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 ‘ 𝑅 ) ) |