Metamath Proof Explorer

Theorem pridlidl

Description: A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Assertion pridlidl ⊢ R ∈ RingOps ∧ P ∈ PrIdl ⁡ R → P ∈ Idl ⁡ R

Proof

Step Hyp Ref Expression
1 eqid ⊢ 1 st ⁡ R = 1 st ⁡ R
2 eqid ⊢ 2 nd ⁡ R = 2 nd ⁡ R
3 eqid ⊢ ran ⁡ 1 st ⁡ R = ran ⁡ 1 st ⁡ R
4 1 2 3 ispridl ⊢ R ∈ RingOps → P ∈ PrIdl ⁡ R ↔ P ∈ Idl ⁡ R ∧ P ≠ ran ⁡ 1 st ⁡ R ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ R y ∈ P → a ⊆ P ∨ b ⊆ P
5 3anass ⊢ P ∈ Idl ⁡ R ∧ P ≠ ran ⁡ 1 st ⁡ R ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ R y ∈ P → a ⊆ P ∨ b ⊆ P ↔ P ∈ Idl ⁡ R ∧ P ≠ ran ⁡ 1 st ⁡ R ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ R y ∈ P → a ⊆ P ∨ b ⊆ P
6 4 5 bitrdi ⊢ R ∈ RingOps → P ∈ PrIdl ⁡ R ↔ P ∈ Idl ⁡ R ∧ P ≠ ran ⁡ 1 st ⁡ R ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ R y ∈ P → a ⊆ P ∨ b ⊆ P
7 6 simprbda ⊢ R ∈ RingOps ∧ P ∈ PrIdl ⁡ R → P ∈ Idl ⁡ R