Metamath Proof Explorer

Theorem cmprmidlmcl

Description: The complement of a prime ideal is multiplicatively closed. (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	cmprmidlmcl	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in (B ∖ P) \land J \in (B ∖ P))) \to I \underset{˙}{\cdot} J \in (B ∖ P)$

Proof

Step	Hyp	Ref	Expression
1		isprmidlc.1	$⊢ B = {Base}_{R}$
2		isprmidlc.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		crngring	$⊢ R \in CRing \to R \in Ring$
4		eldifi	$⊢ I \in (B ∖ P) \to I \in B$
5		eldifi	$⊢ J \in (B ∖ P) \to J \in B$
6	4 5	anim12i	$⊢ (I \in (B ∖ P) \land J \in (B ∖ P)) \to (I \in B \land J \in B)$
7	1 2	ringcl	$⊢ (R \in Ring \land I \in B \land J \in B) \to I \underset{˙}{\cdot} J \in B$
8	7	3expb	$⊢ (R \in Ring \land (I \in B \land J \in B)) \to I \underset{˙}{\cdot} J \in B$
9	3 6 8	syl2an	$⊢ (R \in CRing \land (I \in (B ∖ P) \land J \in (B ∖ P))) \to I \underset{˙}{\cdot} J \in B$
10	9	adantlr	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in (B ∖ P) \land J \in (B ∖ P))) \to I \underset{˙}{\cdot} J \in B$
11		eldifn	$⊢ J \in (B ∖ P) \to \neg J \in P$
12	11	ad2antll	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in (B ∖ P) \land J \in (B ∖ P))) \to \neg J \in P$
13	1 2	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$
14	13	3exp2	$⊢ (R \in CRing \land P \in PrmIdeal (R)) \to (I \in (B ∖ P) \to (J \in B \to (I \underset{˙}{\cdot} J \in P \to J \in P)))$
15	14	imp32	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in (B ∖ P) \land J \in B)) \to (I \underset{˙}{\cdot} J \in P \to J \in P)$
16	15	con3d	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in (B ∖ P) \land J \in B)) \to (\neg J \in P \to \neg I \underset{˙}{\cdot} J \in P)$
17	5 16	sylanr2	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in (B ∖ P) \land J \in (B ∖ P))) \to (\neg J \in P \to \neg I \underset{˙}{\cdot} J \in P)$
18	12 17	mpd	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in (B ∖ P) \land J \in (B ∖ P))) \to \neg I \underset{˙}{\cdot} J \in P$
19	10 18	eldifd	$⊢ ((R \in CRing \land P \in PrmIdeal (R)) \land (I \in (B ∖ P) \land J \in (B ∖ P))) \to I \underset{˙}{\cdot} J \in (B ∖ P)$