Theorem prmidlprop

Description: Property of prime ideals. (Contributed by Thierry Arnoux, 6-Jun-2026)

	Ref	Expression
Hypotheses	prmidlprop.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	prmidlprop.2	⊢ · = ( .r ‘ 𝑅 )
	prmidlprop.3	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	prmidlprop.4	⊢ ( 𝜑 → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) )
	prmidlprop.5	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	prmidlprop.6	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	prmidlprop.7	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝑃 )
Assertion	prmidlprop	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑃 ∨ 𝑌 ∈ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		prmidlprop.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		prmidlprop.2	⊢ · = ( .r ‘ 𝑅 )
3		prmidlprop.3	⊢ ( 𝜑 → 𝑅 ∈ CRing )
4		prmidlprop.4	⊢ ( 𝜑 → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) )
5		prmidlprop.5	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		prmidlprop.6	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		prmidlprop.7	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝑃 )
8		oveq1	⊢ ( 𝑎 = 𝑋 → ( 𝑎 · 𝑏 ) = ( 𝑋 · 𝑏 ) )
9	8	eleq1d	⊢ ( 𝑎 = 𝑋 → ( ( 𝑎 · 𝑏 ) ∈ 𝑃 ↔ ( 𝑋 · 𝑏 ) ∈ 𝑃 ) )
10		eleq1	⊢ ( 𝑎 = 𝑋 → ( 𝑎 ∈ 𝑃 ↔ 𝑋 ∈ 𝑃 ) )
11	10	orbi1d	⊢ ( 𝑎 = 𝑋 → ( ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ↔ ( 𝑋 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) )
12	9 11	imbi12d	⊢ ( 𝑎 = 𝑋 → ( ( ( 𝑎 · 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ↔ ( ( 𝑋 · 𝑏 ) ∈ 𝑃 → ( 𝑋 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
13		oveq2	⊢ ( 𝑏 = 𝑌 → ( 𝑋 · 𝑏 ) = ( 𝑋 · 𝑌 ) )
14	13	eleq1d	⊢ ( 𝑏 = 𝑌 → ( ( 𝑋 · 𝑏 ) ∈ 𝑃 ↔ ( 𝑋 · 𝑌 ) ∈ 𝑃 ) )
15		eleq1	⊢ ( 𝑏 = 𝑌 → ( 𝑏 ∈ 𝑃 ↔ 𝑌 ∈ 𝑃 ) )
16	15	orbi2d	⊢ ( 𝑏 = 𝑌 → ( ( 𝑋 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ↔ ( 𝑋 ∈ 𝑃 ∨ 𝑌 ∈ 𝑃 ) ) )
17	14 16	imbi12d	⊢ ( 𝑏 = 𝑌 → ( ( ( 𝑋 · 𝑏 ) ∈ 𝑃 → ( 𝑋 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ↔ ( ( 𝑋 · 𝑌 ) ∈ 𝑃 → ( 𝑋 ∈ 𝑃 ∨ 𝑌 ∈ 𝑃 ) ) ) )
18	1 2	isprmidlc	⊢ ( 𝑅 ∈ CRing → ( 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) )
19	18	biimpa	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
20	3 4 19	syl2anc	⊢ ( 𝜑 → ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
21	20	simp3d	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) )
22	12 17 21 5 6	rspc2dv	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ∈ 𝑃 → ( 𝑋 ∈ 𝑃 ∨ 𝑌 ∈ 𝑃 ) ) )
23	7 22	mpd	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑃 ∨ 𝑌 ∈ 𝑃 ) )