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

Step	Hyp	Ref	Expression
1		lpival.p	$⊢ P = LPIdeal (R)$
2		lpiss.u	$⊢ U = LIdeal (R)$
3	1 2	islpir	$⊢ R \in LPIR \leftrightarrow (R \in Ring \land U = P)$
4		eqss	$⊢ U = P \leftrightarrow (U \subseteq P \land P \subseteq U)$
5	1 2	lpiss	$⊢ R \in Ring \to P \subseteq U$
6	5	biantrud	$⊢ R \in Ring \to (U \subseteq P \leftrightarrow (U \subseteq P \land P \subseteq U))$
7	4 6	bitr4id	$⊢ R \in Ring \to (U = P \leftrightarrow U \subseteq P)$
8	7	pm5.32i	$⊢ (R \in Ring \land U = P) \leftrightarrow (R \in Ring \land U \subseteq P)$
9	3 8	bitri	$⊢ R \in LPIR \leftrightarrow (R \in Ring \land U \subseteq P)$

Metamath Proof Explorer