Metamath Proof Explorer

Theorem lpirring

Description: Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Assertion lpirring 
|- ( R e. LPIR -> R e. Ring )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( LPIdeal ` R ) = ( LPIdeal ` R )
2 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
3 1 2 islpir 
 |-  ( R e. LPIR <-> ( R e. Ring /\ ( LIdeal ` R ) = ( LPIdeal ` R ) ) )
4 3 simplbi 
 |-  ( R e. LPIR -> R e. Ring )