Metamath Proof Explorer

Theorem prmidlc

Description: Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Hypotheses isprmidlc.1 ⊢ B = Base R
isprmidlc.2 ⊢ · ˙ = ⋅ R
Assertion prmidlc ⊢ R ∈ CRing ∧ P ∈ PrmIdeal ⁡ R ∧ I ∈ B ∧ J ∈ B ∧ I · ˙ J ∈ P → I ∈ P ∨ J ∈ P

Proof

Step Hyp Ref Expression
1 isprmidlc.1 ⊢ B = Base R
2 isprmidlc.2 ⊢ · ˙ = ⋅ R
3 simpr1 ⊢ R ∈ CRing ∧ P ∈ PrmIdeal ⁡ R ∧ I ∈ B ∧ J ∈ B ∧ I · ˙ J ∈ P → I ∈ B
4 simpr2 ⊢ R ∈ CRing ∧ P ∈ PrmIdeal ⁡ R ∧ I ∈ B ∧ J ∈ B ∧ I · ˙ J ∈ P → J ∈ B
5 1 2 isprmidlc ⊢ R ∈ CRing → P ∈ PrmIdeal ⁡ R ↔ P ∈ LIdeal ⁡ R ∧ P ≠ B ∧ ∀ a ∈ B ∀ b ∈ B a · ˙ b ∈ P → a ∈ P ∨ b ∈ P
6 5 biimpa ⊢ R ∈ CRing ∧ P ∈ PrmIdeal ⁡ R → P ∈ LIdeal ⁡ R ∧ P ≠ B ∧ ∀ a ∈ B ∀ b ∈ B a · ˙ b ∈ P → a ∈ P ∨ b ∈ P
7 6 simp3d ⊢ R ∈ CRing ∧ P ∈ PrmIdeal ⁡ R → ∀ a ∈ B ∀ b ∈ B a · ˙ b ∈ P → a ∈ P ∨ b ∈ P
8 7 adantr ⊢ R ∈ CRing ∧ P ∈ PrmIdeal ⁡ R ∧ I ∈ B ∧ J ∈ B ∧ I · ˙ J ∈ P → ∀ a ∈ B ∀ b ∈ B a · ˙ b ∈ P → a ∈ P ∨ b ∈ P
9 simpr3 ⊢ R ∈ CRing ∧ P ∈ PrmIdeal ⁡ R ∧ I ∈ B ∧ J ∈ B ∧ I · ˙ J ∈ P → I · ˙ J ∈ P
10 oveq12 ⊢ a = I ∧ b = J → a · ˙ b = I · ˙ J
11 10 eleq1d ⊢ a = I ∧ b = J → a · ˙ b ∈ P ↔ I · ˙ J ∈ P
12 simpl ⊢ a = I ∧ b = J → a = I
13 12 eleq1d ⊢ a = I ∧ b = J → a ∈ P ↔ I ∈ P
14 simpr ⊢ a = I ∧ b = J → b = J
15 14 eleq1d ⊢ a = I ∧ b = J → b ∈ P ↔ J ∈ P
16 13 15 orbi12d ⊢ a = I ∧ b = J → a ∈ P ∨ b ∈ P ↔ I ∈ P ∨ J ∈ P
17 11 16 imbi12d ⊢ a = I ∧ b = J → a · ˙ b ∈ P → a ∈ P ∨ b ∈ P ↔ I · ˙ J ∈ P → I ∈ P ∨ J ∈ P
18 17 rspc2gv ⊢ I ∈ B ∧ J ∈ B → ∀ a ∈ B ∀ b ∈ B a · ˙ b ∈ P → a ∈ P ∨ b ∈ P → I · ˙ J ∈ P → I ∈ P ∨ J ∈ P
19 18 imp31 ⊢ I ∈ B ∧ J ∈ B ∧ ∀ a ∈ B ∀ b ∈ B a · ˙ b ∈ P → a ∈ P ∨ b ∈ P ∧ I · ˙ J ∈ P → I ∈ P ∨ J ∈ P
20 3 4 8 9 19 syl1111anc ⊢ R ∈ CRing ∧ P ∈ PrmIdeal ⁡ R ∧ I ∈ B ∧ J ∈ B ∧ I · ˙ J ∈ P → I ∈ P ∨ J ∈ P