Theorem rsprprmprmidlb

Description: In an integral domain, an ideal generated by a single element is a prime iff that element is prime. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rsprprmprmidlb.0	$$⊢\underset{\dot{}}{0}=0_R$$
	rsprprmprmidlb.b	$$⊢B={\mathrm{Base}}_R$$
	rsprprmprmidlb.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
	rsprprmprmidlb.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
	rsprprmprmidlb.r	$$⊢\phi \to R\in \mathrm{IDomn}$$
	rsprprmprmidlb.x	$$⊢\phi \to X\in B$$
	rsprprmprmidlb.1	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
Assertion	rsprprmprmidlb	Could not format assertion : No typesetting found for |- ( ph -> ( X e. P <-> ( K ` { X } ) e. ( PrmIdeal ` R ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rsprprmprmidlb.0	$$⊢\underset{\dot{}}{0}=0_R$$
2		rsprprmprmidlb.b	$$⊢B={\mathrm{Base}}_R$$
3		rsprprmprmidlb.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
4		rsprprmprmidlb.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
5		rsprprmprmidlb.r	$$⊢\phi \to R\in \mathrm{IDomn}$$
6		rsprprmprmidlb.x	$$⊢\phi \to X\in B$$
7		rsprprmprmidlb.1	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
8	5	idomcringd	$$⊢\phi \to R\in \mathrm{CRing}$$
9	8	adantr	$$⊢\left(\phi \wedge X\in P\right)\to R\in \mathrm{CRing}$$
10	3	a1i	$$⊢\phi \to P=\mathrm{RPrime}\left(R\right)$$
11	10	eleq2d	$$⊢\phi \to \left(X\in P\leftrightarrow X\in \mathrm{RPrime}\left(R\right)\right)$$
12	11	biimpa	$$⊢\left(\phi \wedge X\in P\right)\to X\in \mathrm{RPrime}\left(R\right)$$
13	4 9 12	rsprprmprmidl	Could not format ( ( ph /\ X e. P ) -> ( K ` { X } ) e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ph /\ X e. P ) -> ( K ` { X } ) e. ( PrmIdeal ` R ) ) with typecode |-
14	5	adantr	Could not format ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> R e. IDomn ) : No typesetting found for |- ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> R e. IDomn ) with typecode |-
15	6	adantr	Could not format ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. B ) : No typesetting found for |- ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. B ) with typecode |-
16		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
17		eqid	$$⊢K\left(\left\{X\right\}\right)=K\left(\left\{X\right\}\right)$$
18	16 4 17 2 15 14	unitpidl1	Could not format ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> ( ( K ` { X } ) = B <-> X e. ( Unit ` R ) ) ) : No typesetting found for |- ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> ( ( K ` { X } ) = B <-> X e. ( Unit ` R ) ) ) with typecode |-
19	18	biimpar	Could not format ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ X e. ( Unit ` R ) ) -> ( K ` { X } ) = B ) : No typesetting found for |- ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ X e. ( Unit ` R ) ) -> ( K ` { X } ) = B ) with typecode |-
20	14	idomringd	Could not format ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> R e. Ring ) : No typesetting found for |- ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> R e. Ring ) with typecode |-
21		eqid	$$⊢{\cdot }_R={\cdot }_R$$
22	2 21	prmidlnr	Could not format ( ( R e. Ring /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> ( K ` { X } ) =/= B ) : No typesetting found for |- ( ( R e. Ring /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> ( K ` { X } ) =/= B ) with typecode |-
23	20 22	sylancom	Could not format ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> ( K ` { X } ) =/= B ) : No typesetting found for |- ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> ( K ` { X } ) =/= B ) with typecode |-
24	23	adantr	Could not format ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ X e. ( Unit ` R ) ) -> ( K ` { X } ) =/= B ) : No typesetting found for |- ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ X e. ( Unit ` R ) ) -> ( K ` { X } ) =/= B ) with typecode |-
25	24	neneqd	Could not format ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ X e. ( Unit ` R ) ) -> -. ( K ` { X } ) = B ) : No typesetting found for |- ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ X e. ( Unit ` R ) ) -> -. ( K ` { X } ) = B ) with typecode |-
26	19 25	pm2.65da	Could not format ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> -. X e. ( Unit ` R ) ) : No typesetting found for |- ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> -. X e. ( Unit ` R ) ) with typecode |-
27		nelsn	$$⊢X\ne \underset{\dot{}}{0}\to \neg X\in \left\{\underset{\dot{}}{0}\right\}$$
28	7 27	syl	$$⊢\phi \to \neg X\in \left\{\underset{\dot{}}{0}\right\}$$
29	28	adantr	Could not format ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> -. X e. { .0. } ) : No typesetting found for |- ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> -. X e. { .0. } ) with typecode |-
30		eqid	$$⊢\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}=\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}$$
31		nelun	$$⊢\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}=\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}\to \left(\neg X\in \left(\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(\neg X\in \mathrm{Unit}\left(R\right)\wedge \neg X\in \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
32	30 31	ax-mp	$$⊢\neg X\in \left(\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(\neg X\in \mathrm{Unit}\left(R\right)\wedge \neg X\in \left\{\underset{\dot{}}{0}\right\}\right)$$
33	26 29 32	sylanbrc	Could not format ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> -. X e. ( ( Unit ` R ) u. { .0. } ) ) : No typesetting found for |- ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> -. X e. ( ( Unit ` R ) u. { .0. } ) ) with typecode |-
34	15 33	eldifd	Could not format ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. ( B \ ( ( Unit ` R ) u. { .0. } ) ) ) : No typesetting found for |- ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. ( B \ ( ( Unit ` R ) u. { .0. } ) ) ) with typecode |-
35		eqid	$$⊢{\parallel }_r\left(R\right)={\parallel }_r\left(R\right)$$
36	20	ad3antrrr	Could not format ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> R e. Ring ) with typecode |-
37	6	ad4antr	Could not format ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> X e. B ) : No typesetting found for |- ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> X e. B ) with typecode |-
38	2 4 35 36 37	ellpi	Could not format ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x e. ( K ` { X } ) <-> X ( ||r ` R ) x ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x e. ( K ` { X } ) <-> X ( ||r ` R ) x ) ) with typecode |-
39	38	biimpa	Could not format ( ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) /\ x e. ( K ` { X } ) ) -> X ( ||r ` R ) x ) : No typesetting found for |- ( ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) /\ x e. ( K ` { X } ) ) -> X ( ||r ` R ) x ) with typecode |-
40	2 4 35 36 37	ellpi	Could not format ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( y e. ( K ` { X } ) <-> X ( ||r ` R ) y ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( y e. ( K ` { X } ) <-> X ( ||r ` R ) y ) ) with typecode |-
41	40	biimpa	Could not format ( ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) /\ y e. ( K ` { X } ) ) -> X ( ||r ` R ) y ) : No typesetting found for |- ( ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) /\ y e. ( K ` { X } ) ) -> X ( ||r ` R ) y ) with typecode |-
42	8	ad4antr	Could not format ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> R e. CRing ) : No typesetting found for |- ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> R e. CRing ) with typecode |-
43		simp-4r	Could not format ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( K ` { X } ) e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( K ` { X } ) e. ( PrmIdeal ` R ) ) with typecode |-
44		simpllr	Could not format ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> x e. B ) : No typesetting found for |- ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> x e. B ) with typecode |-
45		simplr	Could not format ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> y e. B ) : No typesetting found for |- ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> y e. B ) with typecode |-
46	20	ad2antrr	Could not format ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> R e. Ring ) with typecode |-
47	6	ad3antrrr	Could not format ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> X e. B ) : No typesetting found for |- ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> X e. B ) with typecode |-
48	2 4 35 46 47	ellpi	Could not format ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> ( ( x ( .r ` R ) y ) e. ( K ` { X } ) <-> X ( ||r ` R ) ( x ( .r ` R ) y ) ) ) : No typesetting found for |- ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> ( ( x ( .r ` R ) y ) e. ( K ` { X } ) <-> X ( ||r ` R ) ( x ( .r ` R ) y ) ) ) with typecode |-
49	48	biimpar	Could not format ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x ( .r ` R ) y ) e. ( K ` { X } ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x ( .r ` R ) y ) e. ( K ` { X } ) ) with typecode |-
50	2 21	prmidlc	Could not format ( ( ( R e. CRing /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ ( x e. B /\ y e. B /\ ( x ( .r ` R ) y ) e. ( K ` { X } ) ) ) -> ( x e. ( K ` { X } ) \/ y e. ( K ` { X } ) ) ) : No typesetting found for |- ( ( ( R e. CRing /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ ( x e. B /\ y e. B /\ ( x ( .r ` R ) y ) e. ( K ` { X } ) ) ) -> ( x e. ( K ` { X } ) \/ y e. ( K ` { X } ) ) ) with typecode |-
51	42 43 44 45 49 50	syl23anc	Could not format ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x e. ( K ` { X } ) \/ y e. ( K ` { X } ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x e. ( K ` { X } ) \/ y e. ( K ` { X } ) ) ) with typecode |-
52	39 41 51	orim12da	Could not format ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) with typecode |-
53	52	ex	Could not format ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) ) : No typesetting found for |- ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) ) with typecode |-
54	53	anasss	Could not format ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ ( x e. B /\ y e. B ) ) -> ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) ) : No typesetting found for |- ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ ( x e. B /\ y e. B ) ) -> ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) ) with typecode |-
55	54	ralrimivva	Could not format ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> A. x e. B A. y e. B ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) ) : No typesetting found for |- ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> A. x e. B A. y e. B ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) ) with typecode |-
56	2 16 1 35 21	isrprm	$$⊢R\in \mathrm{IDomn}\to \left(X\in \mathrm{RPrime}\left(R\right)\leftrightarrow \left(X\in \left(B\setminus \left(\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge \forall x\in B\forall y\in B\left(X{\parallel }_r\left(R\right)\left(x{\cdot }_{R}y\right)\to \left(X{\parallel }_r\left(R\right)x\vee X{\parallel }_r\left(R\right)y\right)\right)\right)\right)$$
57	56	biimpar	$$⊢\left(R\in \mathrm{IDomn}\wedge \left(X\in \left(B\setminus \left(\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge \forall x\in B\forall y\in B\left(X{\parallel }_r\left(R\right)\left(x{\cdot }_{R}y\right)\to \left(X{\parallel }_r\left(R\right)x\vee X{\parallel }_r\left(R\right)y\right)\right)\right)\right)\to X\in \mathrm{RPrime}\left(R\right)$$
58	14 34 55 57	syl12anc	Could not format ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. ( RPrime ` R ) ) : No typesetting found for |- ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. ( RPrime ` R ) ) with typecode |-
59	58 3	eleqtrrdi	Could not format ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. P ) : No typesetting found for |- ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. P ) with typecode |-
60	13 59	impbida	Could not format ( ph -> ( X e. P <-> ( K ` { X } ) e. ( PrmIdeal ` R ) ) ) : No typesetting found for |- ( ph -> ( X e. P <-> ( K ` { X } ) e. ( PrmIdeal ` R ) ) ) with typecode |-