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 
|- 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 } ) )