Theorem lpirlidllpi

Description: In a principal ideal ring, ideals are principal. (Contributed by Thierry Arnoux, 3-Jun-2025)

	Ref	Expression
Hypotheses	lpirlidllpi.1	$$⊢B={\mathrm{Base}}_R$$
	lpirlidllpi.2	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
	lpirlidllpi.3	$$⊢K=\mathrm{RSpan}\left(R\right)$$
	lpirlidllpi.4	$$⊢\phi \to R\in \mathrm{LPIR}$$
	lpirlidllpi.5	$$⊢\phi \to J\in I$$
Assertion	lpirlidllpi	$$⊢\phi \to \exists x\in BJ=K\left(\left\{x\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lpirlidllpi.1	$$⊢B={\mathrm{Base}}_R$$
2		lpirlidllpi.2	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
3		lpirlidllpi.3	$$⊢K=\mathrm{RSpan}\left(R\right)$$
4		lpirlidllpi.4	$$⊢\phi \to R\in \mathrm{LPIR}$$
5		lpirlidllpi.5	$$⊢\phi \to J\in I$$
6		eqid	$$⊢\mathrm{LPIdeal}\left(R\right)=\mathrm{LPIdeal}\left(R\right)$$
7	6 2	islpir	$$⊢R\in \mathrm{LPIR}\leftrightarrow \left(R\in \mathrm{Ring}\wedge I=\mathrm{LPIdeal}\left(R\right)\right)$$
8	4 7	sylib	$$⊢\phi \to \left(R\in \mathrm{Ring}\wedge I=\mathrm{LPIdeal}\left(R\right)\right)$$
9	8	simpld	$$⊢\phi \to R\in \mathrm{Ring}$$
10	8	simprd	$$⊢\phi \to I=\mathrm{LPIdeal}\left(R\right)$$
11	5 10	eleqtrd	$$⊢\phi \to J\in \mathrm{LPIdeal}\left(R\right)$$
12	6 3 1	islpidl	$$⊢R\in \mathrm{Ring}\to \left(J\in \mathrm{LPIdeal}\left(R\right)\leftrightarrow \exists x\in BJ=K\left(\left\{x\right\}\right)\right)$$
13	12	biimpa	$$⊢\left(R\in \mathrm{Ring}\wedge J\in \mathrm{LPIdeal}\left(R\right)\right)\to \exists x\in BJ=K\left(\left\{x\right\}\right)$$
14	9 11 13	syl2anc	$$⊢\phi \to \exists x\in BJ=K\left(\left\{x\right\}\right)$$