Metamath Proof Explorer

Theorem prmidlidl

Description: A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Assertion prmidlidl ⊢ R ∈ Ring ∧ P ∈ PrmIdeal ⁡ R → P ∈ LIdeal ⁡ R

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base R = Base R
2 eqid ⊢ ⋅ R = ⋅ R
3 1 2 isprmidl ⊢ R ∈ Ring → P ∈ PrmIdeal ⁡ R ↔ P ∈ LIdeal ⁡ R ∧ P ≠ Base R ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x ⋅ R y ∈ P → a ⊆ P ∨ b ⊆ P
4 3 biimpa ⊢ R ∈ Ring ∧ P ∈ PrmIdeal ⁡ R → P ∈ LIdeal ⁡ R ∧ P ≠ Base R ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x ⋅ R y ∈ P → a ⊆ P ∨ b ⊆ P
5 4 simp1d ⊢ R ∈ Ring ∧ P ∈ PrmIdeal ⁡ R → P ∈ LIdeal ⁡ R