Theorem rprmasso

Description: In an integral domain, the associate of a prime is a prime. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rprmasso.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rprmasso.p	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
	rprmasso.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
	rprmasso.r	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
	rprmasso.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	rprmasso.1	⊢ ( 𝜑 → 𝑋 ∥ 𝑌 )
	rprmasso.y	⊢ ( 𝜑 → 𝑌 ∥ 𝑋 )
Assertion	rprmasso	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		rprmasso.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rprmasso.p	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
3		rprmasso.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
4		rprmasso.r	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
5		rprmasso.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6		rprmasso.1	⊢ ( 𝜑 → 𝑋 ∥ 𝑌 )
7		rprmasso.y	⊢ ( 𝜑 → 𝑌 ∥ 𝑋 )
8		eqid	⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
9	1 2 4 5	rprmcl	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
10	1 3	dvdsrcl	⊢ ( 𝑌 ∥ 𝑋 → 𝑌 ∈ 𝐵 )
11	7 10	syl	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
12	4	idomringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
13	1 8 3 9 11 12	rspsnasso	⊢ ( 𝜑 → ( ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ↔ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑌 } ) = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) )
14	6 7 13	mpbi2and	⊢ ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑌 } ) = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) )
15	4	idomcringd	⊢ ( 𝜑 → 𝑅 ∈ CRing )
16	5 2	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( RPrime ‘ 𝑅 ) )
17	8 15 16	rsprprmprmidl	⊢ ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) )
18	14 17	eqeltrd	⊢ ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑌 } ) ∈ ( PrmIdeal ‘ 𝑅 ) )
19		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
20	2 19 4 5	rprmnz	⊢ ( 𝜑 → 𝑋 ≠ ( 0g ‘ 𝑅 ) )
21	12	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
22	9	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑅 ) ) → 𝑋 ∈ 𝐵 )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑅 ) ) → 𝑌 = ( 0g ‘ 𝑅 ) )
24	7	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑅 ) ) → 𝑌 ∥ 𝑋 )
25	23 24	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∥ 𝑋 )
26	1 3 19	dvdsr02	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 0g ‘ 𝑅 ) ∥ 𝑋 ↔ 𝑋 = ( 0g ‘ 𝑅 ) ) )
27	26	biimpa	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ ( 0g ‘ 𝑅 ) ∥ 𝑋 ) → 𝑋 = ( 0g ‘ 𝑅 ) )
28	21 22 25 27	syl21anc	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑅 ) ) → 𝑋 = ( 0g ‘ 𝑅 ) )
29	20 28	mteqand	⊢ ( 𝜑 → 𝑌 ≠ ( 0g ‘ 𝑅 ) )
30	19 1 2 8 4 11 29	rsprprmprmidlb	⊢ ( 𝜑 → ( 𝑌 ∈ 𝑃 ↔ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑌 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) )
31	18 30	mpbird	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )