Metamath Proof Explorer

Theorem prmidlprop

Description: Property of prime ideals. (Contributed by Thierry Arnoux, 6-Jun-2026)

Ref Expression
Hypotheses prmidlprop.1 ⊢ B = Base R
prmidlprop.2 ⊢ · ˙ = ⋅ R
prmidlprop.3 ⊢ φ → R ∈ CRing
prmidlprop.4 ⊢ φ → P ∈ PrmIdeal ⁡ R
prmidlprop.5 ⊢ φ → X ∈ B
prmidlprop.6 ⊢ φ → Y ∈ B
prmidlprop.7 ⊢ φ → X · ˙ Y ∈ P
Assertion prmidlprop ⊢ φ → X ∈ P ∨ Y ∈ P

Proof

Step Hyp Ref Expression
1 prmidlprop.1 ⊢ B = Base R
2 prmidlprop.2 ⊢ · ˙ = ⋅ R
3 prmidlprop.3 ⊢ φ → R ∈ CRing
4 prmidlprop.4 ⊢ φ → P ∈ PrmIdeal ⁡ R
5 prmidlprop.5 ⊢ φ → X ∈ B
6 prmidlprop.6 ⊢ φ → Y ∈ B
7 prmidlprop.7 ⊢ φ → X · ˙ Y ∈ P
8 oveq1 ⊢ a = X → a · ˙ b = X · ˙ b
9 8 eleq1d ⊢ a = X → a · ˙ b ∈ P ↔ X · ˙ b ∈ P
10 eleq1 ⊢ a = X → a ∈ P ↔ X ∈ P
11 10 orbi1d ⊢ a = X → a ∈ P ∨ b ∈ P ↔ X ∈ P ∨ b ∈ P
12 9 11 imbi12d ⊢ a = X → a · ˙ b ∈ P → a ∈ P ∨ b ∈ P ↔ X · ˙ b ∈ P → X ∈ P ∨ b ∈ P
13 oveq2 ⊢ b = Y → X · ˙ b = X · ˙ Y
14 13 eleq1d ⊢ b = Y → X · ˙ b ∈ P ↔ X · ˙ Y ∈ P
15 eleq1 ⊢ b = Y → b ∈ P ↔ Y ∈ P
16 15 orbi2d ⊢ b = Y → X ∈ P ∨ b ∈ P ↔ X ∈ P ∨ Y ∈ P
17 14 16 imbi12d ⊢ b = Y → X · ˙ b ∈ P → X ∈ P ∨ b ∈ P ↔ X · ˙ Y ∈ P → X ∈ P ∨ Y ∈ P
18 1 2 isprmidlc ⊢ R ∈ CRing → P ∈ PrmIdeal ⁡ R ↔ P ∈ LIdeal ⁡ R ∧ P ≠ B ∧ ∀ a ∈ B ∀ b ∈ B a · ˙ b ∈ P → a ∈ P ∨ b ∈ P
19 18 biimpa ⊢ R ∈ CRing ∧ P ∈ PrmIdeal ⁡ R → P ∈ LIdeal ⁡ R ∧ P ≠ B ∧ ∀ a ∈ B ∀ b ∈ B a · ˙ b ∈ P → a ∈ P ∨ b ∈ P
20 3 4 19 syl2anc ⊢ φ → P ∈ LIdeal ⁡ R ∧ P ≠ B ∧ ∀ a ∈ B ∀ b ∈ B a · ˙ b ∈ P → a ∈ P ∨ b ∈ P
21 20 simp3d ⊢ φ → ∀ a ∈ B ∀ b ∈ B a · ˙ b ∈ P → a ∈ P ∨ b ∈ P
22 12 17 21 5 6 rspc2dv ⊢ φ → X · ˙ Y ∈ P → X ∈ P ∨ Y ∈ P
23 7 22 mpd ⊢ φ → X ∈ P ∨ Y ∈ P