This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝐽 = ( 𝐾 ‘ { 𝑥 } ) )