Metamath Proof Explorer

Theorem pridlc2

Description: Obsolete theorem, use prmidlc2 instead. Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses ispridlc.1 ⊢ G = 1 st ⁡ R
ispridlc.2 ⊢ H = 2 nd ⁡ R
ispridlc.3 ⊢ X = ran ⁡ G
Assertion pridlc2 ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∖ P ∧ B ∈ X ∧ A H B ∈ 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 eldifn ⊢ A ∈ X ∖ P → ¬ A ∈ P
5 4 3ad2ant1 ⊢ A ∈ X ∖ P ∧ B ∈ X ∧ A H B ∈ P → ¬ A ∈ P
6 5 adantl ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∖ P ∧ B ∈ X ∧ A H B ∈ P → ¬ A ∈ P
7 eldifi ⊢ A ∈ X ∖ P → A ∈ X
8 1 2 3 pridlc ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∧ B ∈ X ∧ A H B ∈ P → A ∈ P ∨ B ∈ P
9 8 ord ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∧ B ∈ X ∧ A H B ∈ P → ¬ A ∈ P → B ∈ P
10 7 9 syl3anr1 ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∖ P ∧ B ∈ X ∧ A H B ∈ P → ¬ A ∈ P → B ∈ P
11 6 10 mpd ⊢ R ∈ CRingOps ∧ P ∈ PrIdl ⁡ R ∧ A ∈ X ∖ P ∧ B ∈ X ∧ A H B ∈ P → B ∈ P