Theorem lpirlidllpi

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

	Ref	Expression
Hypotheses	lpirlidllpi.1	|- B = ( Base ` R )
	lpirlidllpi.2	|- I = ( LIdeal ` R )
	lpirlidllpi.3	|- K = ( RSpan ` R )
	lpirlidllpi.4	|- ( ph -> R e. LPIR )
	lpirlidllpi.5	|- ( ph -> J e. I )
Assertion	lpirlidllpi	|- ( ph -> E. x e. B J = ( K ` { x } ) )

Proof

Step	Hyp	Ref	Expression
1		lpirlidllpi.1	|- B = ( Base ` R )
2		lpirlidllpi.2	|- I = ( LIdeal ` R )
3		lpirlidllpi.3	|- K = ( RSpan ` R )
4		lpirlidllpi.4	|- ( ph -> R e. LPIR )
5		lpirlidllpi.5	|- ( ph -> J e. I )
6		eqid	|- ( LPIdeal ` R ) = ( LPIdeal ` R )
7	6 2	islpir	|- ( R e. LPIR <-> ( R e. Ring /\ I = ( LPIdeal ` R ) ) )
8	4 7	sylib	|- ( ph -> ( R e. Ring /\ I = ( LPIdeal ` R ) ) )
9	8	simpld	|- ( ph -> R e. Ring )
10	8	simprd	|- ( ph -> I = ( LPIdeal ` R ) )
11	5 10	eleqtrd	|- ( ph -> J e. ( LPIdeal ` R ) )
12	6 3 1	islpidl	|- ( R e. Ring -> ( J e. ( LPIdeal ` R ) <-> E. x e. B J = ( K ` { x } ) ) )
13	12	biimpa	|- ( ( R e. Ring /\ J e. ( LPIdeal ` R ) ) -> E. x e. B J = ( K ` { x } ) )
14	9 11 13	syl2anc	|- ( ph -> E. x e. B J = ( K ` { x } ) )