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

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