Theorem lpirring

Description: Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Assertion	lpirring	$$⊢R\in \mathrm{LPIR}\to R\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{LPIdeal}\left(R\right)=\mathrm{LPIdeal}\left(R\right)$$
2		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
3	1 2	islpir	$$⊢R\in \mathrm{LPIR}\leftrightarrow \left(R\in \mathrm{Ring}\wedge \mathrm{LIdeal}\left(R\right)=\mathrm{LPIdeal}\left(R\right)\right)$$
4	3	simplbi	$$⊢R\in \mathrm{LPIR}\to R\in \mathrm{Ring}$$