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