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=\mathrm{LPIdeal}\left(R\right)$$
	lpiss.u	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
Assertion	islpir	$$⊢R\in \mathrm{LPIR}\leftrightarrow \left(R\in \mathrm{Ring}\wedge U=P\right)$$

Proof

Step	Hyp	Ref	Expression
1		lpival.p	$$⊢P=\mathrm{LPIdeal}\left(R\right)$$
2		lpiss.u	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
3		fveq2	$$⊢r=R\to \mathrm{LIdeal}\left(r\right)=\mathrm{LIdeal}\left(R\right)$$
4		fveq2	$$⊢r=R\to \mathrm{LPIdeal}\left(r\right)=\mathrm{LPIdeal}\left(R\right)$$
5	3 4	eqeq12d	$$⊢r=R\to \left(\mathrm{LIdeal}\left(r\right)=\mathrm{LPIdeal}\left(r\right)\leftrightarrow \mathrm{LIdeal}\left(R\right)=\mathrm{LPIdeal}\left(R\right)\right)$$
6	2 1	eqeq12i	$$⊢U=P\leftrightarrow \mathrm{LIdeal}\left(R\right)=\mathrm{LPIdeal}\left(R\right)$$
7	5 6	bitr4di	$$⊢r=R\to \left(\mathrm{LIdeal}\left(r\right)=\mathrm{LPIdeal}\left(r\right)\leftrightarrow U=P\right)$$
8		df-lpir	$$⊢\mathrm{LPIR}=\left\{r\in \mathrm{Ring}|\mathrm{LIdeal}\left(r\right)=\mathrm{LPIdeal}\left(r\right)\right\}$$
9	7 8	elrab2	$$⊢R\in \mathrm{LPIR}\leftrightarrow \left(R\in \mathrm{Ring}\wedge U=P\right)$$