pridlc2

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	pridlc2	$⊢ ((R \in CRingOps \land P \in PrIdl (R)) \land (A \in (X ∖ P) \land B \in X \land A H B \in P)) \to B \in P$

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 \in (X ∖ P) \to \neg A \in P$
5	4	3ad2ant1	$⊢ (A \in (X ∖ P) \land B \in X \land A H B \in P) \to \neg A \in P$
6	5	adantl	$⊢ ((R \in CRingOps \land P \in PrIdl (R)) \land (A \in (X ∖ P) \land B \in X \land A H B \in P)) \to \neg A \in P$
7		eldifi	$⊢ A \in (X ∖ P) \to A \in X$
8	1 2 3	pridlc	$⊢ ((R \in CRingOps \land P \in PrIdl (R)) \land (A \in X \land B \in X \land A H B \in P)) \to (A \in P \lor B \in P)$
9	8	ord	$⊢ ((R \in CRingOps \land P \in PrIdl (R)) \land (A \in X \land B \in X \land A H B \in P)) \to (\neg A \in P \to B \in P)$
10	7 9	syl3anr1	$⊢ ((R \in CRingOps \land P \in PrIdl (R)) \land (A \in (X ∖ P) \land B \in X \land A H B \in P)) \to (\neg A \in P \to B \in P)$
11	6 10	mpd	$⊢ ((R \in CRingOps \land P \in PrIdl (R)) \land (A \in (X ∖ P) \land B \in X \land A H B \in P)) \to B \in P$

Metamath Proof Explorer