Theorem lpirlidllpi

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

	Ref	Expression
Hypotheses	lpirlidllpi.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	lpirlidllpi.2	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
	lpirlidllpi.3	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	lpirlidllpi.4	⊢ ( 𝜑 → 𝑅 ∈ LPIR )
	lpirlidllpi.5	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
Assertion	lpirlidllpi	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝐽 = ( 𝐾 ‘ { 𝑥 } ) )

Proof

Step	Hyp	Ref	Expression
1		lpirlidllpi.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		lpirlidllpi.2	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
3		lpirlidllpi.3	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
4		lpirlidllpi.4	⊢ ( 𝜑 → 𝑅 ∈ LPIR )
5		lpirlidllpi.5	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
6		eqid	⊢ ( LPIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 )
7	6 2	islpir	⊢ ( 𝑅 ∈ LPIR ↔ ( 𝑅 ∈ Ring ∧ 𝐼 = ( LPIdeal ‘ 𝑅 ) ) )
8	4 7	sylib	⊢ ( 𝜑 → ( 𝑅 ∈ Ring ∧ 𝐼 = ( LPIdeal ‘ 𝑅 ) ) )
9	8	simpld	⊢ ( 𝜑 → 𝑅 ∈ Ring )
10	8	simprd	⊢ ( 𝜑 → 𝐼 = ( LPIdeal ‘ 𝑅 ) )
11	5 10	eleqtrd	⊢ ( 𝜑 → 𝐽 ∈ ( LPIdeal ‘ 𝑅 ) )
12	6 3 1	islpidl	⊢ ( 𝑅 ∈ Ring → ( 𝐽 ∈ ( LPIdeal ‘ 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐵 𝐽 = ( 𝐾 ‘ { 𝑥 } ) ) )
13	12	biimpa	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐽 ∈ ( LPIdeal ‘ 𝑅 ) ) → ∃ 𝑥 ∈ 𝐵 𝐽 = ( 𝐾 ‘ { 𝑥 } ) )
14	9 11 13	syl2anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝐽 = ( 𝐾 ‘ { 𝑥 } ) )