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	$$⊢B={\mathrm{Base}}_R$$
	rprmasso.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
	rprmasso.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
	rprmasso.r	$$⊢\phi \to R\in \mathrm{IDomn}$$
	rprmasso.x	$$⊢\phi \to X\in P$$
	rprmasso.1	$$⊢\phi \to X\underset{\dot{}}{\parallel }Y$$
	rprmasso.y	$$⊢\phi \to Y\underset{\dot{}}{\parallel }X$$
Assertion	rprmasso	$$⊢\phi \to Y\in P$$

Proof

Step	Hyp	Ref	Expression
1		rprmasso.b	$$⊢B={\mathrm{Base}}_R$$
2		rprmasso.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
3		rprmasso.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
4		rprmasso.r	$$⊢\phi \to R\in \mathrm{IDomn}$$
5		rprmasso.x	$$⊢\phi \to X\in P$$
6		rprmasso.1	$$⊢\phi \to X\underset{\dot{}}{\parallel }Y$$
7		rprmasso.y	$$⊢\phi \to Y\underset{\dot{}}{\parallel }X$$
8		eqid	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{RSpan}\left(R\right)$$
9	1 2 4 5	rprmcl	$$⊢\phi \to X\in B$$
10	1 3	dvdsrcl	$$⊢Y\underset{\dot{}}{\parallel }X\to Y\in B$$
11	7 10	syl	$$⊢\phi \to Y\in B$$
12	4	idomringd	$$⊢\phi \to R\in \mathrm{Ring}$$
13	1 8 3 9 11 12	rspsnasso	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\parallel }Y\wedge Y\underset{\dot{}}{\parallel }X\right)\leftrightarrow \mathrm{RSpan}\left(R\right)\left(\left\{Y\right\}\right)=\mathrm{RSpan}\left(R\right)\left(\left\{X\right\}\right)\right)$$
14	6 7 13	mpbi2and	$$⊢\phi \to \mathrm{RSpan}\left(R\right)\left(\left\{Y\right\}\right)=\mathrm{RSpan}\left(R\right)\left(\left\{X\right\}\right)$$
15	4	idomcringd	$$⊢\phi \to R\in \mathrm{CRing}$$
16	5 2	eleqtrdi	$$⊢\phi \to X\in \mathrm{RPrime}\left(R\right)$$
17	8 15 16	rsprprmprmidl	Could not format ( ph -> ( ( RSpan ` R ) ` { X } ) e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ph -> ( ( RSpan ` R ) ` { X } ) e. ( PrmIdeal ` R ) ) with typecode |-
18	14 17	eqeltrd	Could not format ( ph -> ( ( RSpan ` R ) ` { Y } ) e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ph -> ( ( RSpan ` R ) ` { Y } ) e. ( PrmIdeal ` R ) ) with typecode |-
19		eqid	$$⊢0_R=0_R$$
20	2 19 4 5	rprmnz	$$⊢\phi \to X\ne 0_R$$
21	12	adantr	$$⊢\left(\phi \wedge Y=0_R\right)\to R\in \mathrm{Ring}$$
22	9	adantr	$$⊢\left(\phi \wedge Y=0_R\right)\to X\in B$$
23		simpr	$$⊢\left(\phi \wedge Y=0_R\right)\to Y=0_R$$
24	7	adantr	$$⊢\left(\phi \wedge Y=0_R\right)\to Y\underset{\dot{}}{\parallel }X$$
25	23 24	eqbrtrrd	$$⊢\left(\phi \wedge Y=0_R\right)\to 0_R\underset{\dot{}}{\parallel }X$$
26	1 3 19	dvdsr02	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(0_R\underset{\dot{}}{\parallel }X\leftrightarrow X=0_R\right)$$
27	26	biimpa	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge 0_R\underset{\dot{}}{\parallel }X\right)\to X=0_R$$
28	21 22 25 27	syl21anc	$$⊢\left(\phi \wedge Y=0_R\right)\to X=0_R$$
29	20 28	mteqand	$$⊢\phi \to Y\ne 0_R$$
30	19 1 2 8 4 11 29	rsprprmprmidlb	Could not format ( ph -> ( Y e. P <-> ( ( RSpan ` R ) ` { Y } ) e. ( PrmIdeal ` R ) ) ) : No typesetting found for |- ( ph -> ( Y e. P <-> ( ( RSpan ` R ) ` { Y } ) e. ( PrmIdeal ` R ) ) ) with typecode |-
31	18 30	mpbird	$$⊢\phi \to Y\in P$$