Metamath Proof Explorer


Theorem islpir

Description: Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lpival.p
|- P = ( LPIdeal ` R )
lpiss.u
|- U = ( LIdeal ` R )
Assertion islpir
|- ( R e. LPIR <-> ( R e. Ring /\ U = P ) )

Proof

Step Hyp Ref Expression
1 lpival.p
 |-  P = ( LPIdeal ` R )
2 lpiss.u
 |-  U = ( LIdeal ` R )
3 fveq2
 |-  ( r = R -> ( LIdeal ` r ) = ( LIdeal ` R ) )
4 fveq2
 |-  ( r = R -> ( LPIdeal ` r ) = ( LPIdeal ` R ) )
5 3 4 eqeq12d
 |-  ( r = R -> ( ( LIdeal ` r ) = ( LPIdeal ` r ) <-> ( LIdeal ` R ) = ( LPIdeal ` R ) ) )
6 2 1 eqeq12i
 |-  ( U = P <-> ( LIdeal ` R ) = ( LPIdeal ` R ) )
7 5 6 bitr4di
 |-  ( r = R -> ( ( LIdeal ` r ) = ( LPIdeal ` r ) <-> U = P ) )
8 df-lpir
 |-  LPIR = { r e. Ring | ( LIdeal ` r ) = ( LPIdeal ` r ) }
9 7 8 elrab2
 |-  ( R e. LPIR <-> ( R e. Ring /\ U = P ) )