Metamath Proof Explorer

Theorem pridlc

Description: Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011)

Ref Expression
Hypotheses ispridlc.1 ⊢ G = 1 st ⁡ R
ispridlc.2 ⊢ H = 2 nd ⁡ R
ispridlc.3 ⊢ X = ran ⁡ G
Assertion pridlc ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∧ B ∈ X ∧ A H B ∈ P → A ∈ P ∨ B ∈ P

Proof

Step Hyp Ref Expression
1 ispridlc.1 ⊢ G = 1 st ⁡ R
2 ispridlc.2 ⊢ H = 2 nd ⁡ R
3 ispridlc.3 ⊢ X = ran ⁡ G
4 1 2 3 ispridlc ⊢ R ∈ CRingOps → P ∈ PrIdl ⁡ R ↔ P ∈ Idl ⁡ R ∧ P ≠ X ∧ ∀ a ∈ X ∀ b ∈ X a H b ∈ P → a ∈ P ∨ b ∈ P
5 4 biimpa ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R → P ∈ Idl ⁡ R ∧ P ≠ X ∧ ∀ a ∈ X ∀ b ∈ X a H b ∈ P → a ∈ P ∨ b ∈ P
6 5 simp3d ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R → ∀ a ∈ X ∀ b ∈ X a H b ∈ P → a ∈ P ∨ b ∈ P
7 oveq1 ⊢ a = A → a H b = A H b
8 7 eleq1d ⊢ a = A → a H b ∈ P ↔ A H b ∈ P
9 eleq1 ⊢ a = A → a ∈ P ↔ A ∈ P
10 9 orbi1d ⊢ a = A → a ∈ P ∨ b ∈ P ↔ A ∈ P ∨ b ∈ P
11 8 10 imbi12d ⊢ a = A → a H b ∈ P → a ∈ P ∨ b ∈ P ↔ A H b ∈ P → A ∈ P ∨ b ∈ P
12 oveq2 ⊢ b = B → A H b = A H B
13 12 eleq1d ⊢ b = B → A H b ∈ P ↔ A H B ∈ P
14 eleq1 ⊢ b = B → b ∈ P ↔ B ∈ P
15 14 orbi2d ⊢ b = B → A ∈ P ∨ b ∈ P ↔ A ∈ P ∨ B ∈ P
16 13 15 imbi12d ⊢ b = B → A H b ∈ P → A ∈ P ∨ b ∈ P ↔ A H B ∈ P → A ∈ P ∨ B ∈ P
17 11 16 rspc2v ⊢ A ∈ X ∧ B ∈ X → ∀ a ∈ X ∀ b ∈ X a H b ∈ P → a ∈ P ∨ b ∈ P → A H B ∈ P → A ∈ P ∨ B ∈ P
18 17 com12 ⊢ ∀ a ∈ X ∀ b ∈ X a H b ∈ P → a ∈ P ∨ b ∈ P → A ∈ X ∧ B ∈ X → A H B ∈ P → A ∈ P ∨ B ∈ P
19 18 expd ⊢ ∀ a ∈ X ∀ b ∈ X a H b ∈ P → a ∈ P ∨ b ∈ P → A ∈ X → B ∈ X → A H B ∈ P → A ∈ P ∨ B ∈ P
20 19 3imp2 ⊢ ∀ a ∈ X ∀ b ∈ X a H b ∈ P → a ∈ P ∨ b ∈ P ∧ A ∈ X ∧ B ∈ X ∧ A H B ∈ P → A ∈ P ∨ B ∈ P
21 6 20 sylan ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∧ B ∈ X ∧ A H B ∈ P → A ∈ P ∨ B ∈ P