Metamath Proof Explorer


Theorem islpir2

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 islpir2
|- ( R e. LPIR <-> ( R e. Ring /\ U C_ P ) )

Proof

Step Hyp Ref Expression
1 lpival.p
 |-  P = ( LPIdeal ` R )
2 lpiss.u
 |-  U = ( LIdeal ` R )
3 1 2 islpir
 |-  ( R e. LPIR <-> ( R e. Ring /\ U = P ) )
4 eqss
 |-  ( U = P <-> ( U C_ P /\ P C_ U ) )
5 1 2 lpiss
 |-  ( R e. Ring -> P C_ U )
6 5 biantrud
 |-  ( R e. Ring -> ( U C_ P <-> ( U C_ P /\ P C_ U ) ) )
7 4 6 bitr4id
 |-  ( R e. Ring -> ( U = P <-> U C_ P ) )
8 7 pm5.32i
 |-  ( ( R e. Ring /\ U = P ) <-> ( R e. Ring /\ U C_ P ) )
9 3 8 bitri
 |-  ( R e. LPIR <-> ( R e. Ring /\ U C_ P ) )