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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isprmidlc.2	⊢ · = ( .r ‘ 𝑅 )
Assertion	cmprmidlmcl	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ ( 𝐵 ∖ 𝑃 ) ) ) → ( 𝐼 · 𝐽 ) ∈ ( 𝐵 ∖ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		isprmidlc.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isprmidlc.2	⊢ · = ( .r ‘ 𝑅 )
3		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
4		eldifi	⊢ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) → 𝐼 ∈ 𝐵 )
5		eldifi	⊢ ( 𝐽 ∈ ( 𝐵 ∖ 𝑃 ) → 𝐽 ∈ 𝐵 )
6	4 5	anim12i	⊢ ( ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ ( 𝐵 ∖ 𝑃 ) ) → ( 𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ) )
7	1 2	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ) → ( 𝐼 · 𝐽 ) ∈ 𝐵 )
8	7	3expb	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ) ) → ( 𝐼 · 𝐽 ) ∈ 𝐵 )
9	3 6 8	syl2an	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ ( 𝐵 ∖ 𝑃 ) ) ) → ( 𝐼 · 𝐽 ) ∈ 𝐵 )
10	9	adantlr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ ( 𝐵 ∖ 𝑃 ) ) ) → ( 𝐼 · 𝐽 ) ∈ 𝐵 )
11		eldifn	⊢ ( 𝐽 ∈ ( 𝐵 ∖ 𝑃 ) → ¬ 𝐽 ∈ 𝑃 )
12	11	ad2antll	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ ( 𝐵 ∖ 𝑃 ) ) ) → ¬ 𝐽 ∈ 𝑃 )
13	1 2	prmidlc2	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) ) → 𝐽 ∈ 𝑃 )
14	13	3exp2	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) → ( 𝐽 ∈ 𝐵 → ( ( 𝐼 · 𝐽 ) ∈ 𝑃 → 𝐽 ∈ 𝑃 ) ) ) )
15	14	imp32	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ 𝐵 ) ) → ( ( 𝐼 · 𝐽 ) ∈ 𝑃 → 𝐽 ∈ 𝑃 ) )
16	15	con3d	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ 𝐵 ) ) → ( ¬ 𝐽 ∈ 𝑃 → ¬ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) )
17	5 16	sylanr2	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ ( 𝐵 ∖ 𝑃 ) ) ) → ( ¬ 𝐽 ∈ 𝑃 → ¬ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) )
18	12 17	mpd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ ( 𝐵 ∖ 𝑃 ) ) ) → ¬ ( 𝐼 · 𝐽 ) ∈ 𝑃 )
19	10 18	eldifd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ ( 𝐵 ∖ 𝑃 ) ) ) → ( 𝐼 · 𝐽 ) ∈ ( 𝐵 ∖ 𝑃 ) )