prmidlc2

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

	Ref	Expression
Hypotheses	isprmidlc.1	$⊢ B = {Base}_{R}$
	isprmidlc.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	prmidlc2	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in (B ∖ P) \land J \in B \land I \underset{˙}{\cdot} J \in P)) \to J \in P$

Step	Hyp	Ref	Expression
1		isprmidlc.1	$⊢ B = {Base}_{R}$
2		isprmidlc.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		eldifn	$⊢ I \in (B ∖ P) \to \neg I \in P$
4	3	3ad2ant1	$⊢ (I \in (B ∖ P) \land J \in B \land I \underset{˙}{\cdot} J \in P) \to \neg I \in P$
5	4	adantl	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in (B ∖ P) \land J \in B \land I \underset{˙}{\cdot} J \in P)) \to \neg I \in P$
6		eldifi	$⊢ I \in (B ∖ P) \to I \in B$
7	1 2	prmidlc	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in B \land J \in B \land I \underset{˙}{\cdot} J \in P)) \to (I \in P \lor J \in P)$
8	7	ord	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in B \land J \in B \land I \underset{˙}{\cdot} J \in P)) \to (\neg I \in P \to J \in P)$
9	6 8	syl3anr1	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in (B ∖ P) \land J \in B \land I \underset{˙}{\cdot} J \in P)) \to (\neg I \in P \to J \in P)$
10	5 9	mpd	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in (B ∖ P) \land J \in B \land I \underset{˙}{\cdot} J \in P)) \to J \in P$

Metamath Proof Explorer