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