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 \in LPIR \leftrightarrow (R \in Ring \land U = P)$

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

Metamath Proof Explorer