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