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

Proof

Step	Hyp	Ref	Expression
1		isprmidlc.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isprmidlc.2	⊢ · = ( .r ‘ 𝑅 )
3		eldifn	⊢ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) → ¬ 𝐼 ∈ 𝑃 )
4	3	3ad2ant1	⊢ ( ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) → ¬ 𝐼 ∈ 𝑃 )
5	4	adantl	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) ) → ¬ 𝐼 ∈ 𝑃 )
6		eldifi	⊢ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) → 𝐼 ∈ 𝐵 )
7	1 2	prmidlc	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) ) → ( 𝐼 ∈ 𝑃 ∨ 𝐽 ∈ 𝑃 ) )
8	7	ord	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) ) → ( ¬ 𝐼 ∈ 𝑃 → 𝐽 ∈ 𝑃 ) )
9	6 8	syl3anr1	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) ) → ( ¬ 𝐼 ∈ 𝑃 → 𝐽 ∈ 𝑃 ) )
10	5 9	mpd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐼 · 𝐽 ) ∈ 𝑃 ) ) → 𝐽 ∈ 𝑃 )