This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isprmidl

Description: The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Hypotheses prmidlval.1 ⊢ B = Base R
prmidlval.2 ⊢ · ˙ = ⋅ R
Assertion isprmidl ⊢ R ∈ Ring → P ∈ PrmIdeal ⁡ R ↔ P ∈ LIdeal ⁡ R ∧ P ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ P → a ⊆ P ∨ b ⊆ P

Proof

Step Hyp Ref Expression
1 prmidlval.1 ⊢ B = Base R
2 prmidlval.2 ⊢ · ˙ = ⋅ R
3 1 2 prmidlval ⊢ R ∈ Ring → PrmIdeal ⁡ R = i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
4 3 eleq2d ⊢ R ∈ Ring → P ∈ PrmIdeal ⁡ R ↔ P ∈ i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
5 neeq1 ⊢ i = P → i ≠ B ↔ P ≠ B
6 eleq2 ⊢ i = P → x · ˙ y ∈ i ↔ x · ˙ y ∈ P
7 6 2ralbidv ⊢ i = P → ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i ↔ ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ P
8 sseq2 ⊢ i = P → a ⊆ i ↔ a ⊆ P
9 sseq2 ⊢ i = P → b ⊆ i ↔ b ⊆ P
10 8 9 orbi12d ⊢ i = P → a ⊆ i ∨ b ⊆ i ↔ a ⊆ P ∨ b ⊆ P
11 7 10 imbi12d ⊢ i = P → ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i ↔ ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ P → a ⊆ P ∨ b ⊆ P
12 11 2ralbidv ⊢ i = P → ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i ↔ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ P → a ⊆ P ∨ b ⊆ P
13 5 12 anbi12d ⊢ i = P → i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i ↔ P ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ P → a ⊆ P ∨ b ⊆ P
14 13 elrab ⊢ P ∈ i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i ↔ P ∈ LIdeal ⁡ R ∧ P ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ P → a ⊆ P ∨ b ⊆ P
15 4 14 bitrdi ⊢ R ∈ Ring → P ∈ PrmIdeal ⁡ R ↔ P ∈ LIdeal ⁡ R ∧ P ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ P → a ⊆ P ∨ b ⊆ P
16 3anass ⊢ P ∈ LIdeal ⁡ R ∧ P ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ P → a ⊆ P ∨ b ⊆ P ↔ P ∈ LIdeal ⁡ R ∧ P ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ P → a ⊆ P ∨ b ⊆ P
17 15 16 bitr4di ⊢ R ∈ Ring → P ∈ PrmIdeal ⁡ R ↔ P ∈ LIdeal ⁡ R ∧ P ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ P → a ⊆ P ∨ b ⊆ P