Theorem islpir2

Description: Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lpival.p	⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
	lpiss.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
Assertion	islpir2	⊢ ( 𝑅 ∈ LPIR ↔ ( 𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		lpival.p	⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
2		lpiss.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
3	1 2	islpir	⊢ ( 𝑅 ∈ LPIR ↔ ( 𝑅 ∈ Ring ∧ 𝑈 = 𝑃 ) )
4		eqss	⊢ ( 𝑈 = 𝑃 ↔ ( 𝑈 ⊆ 𝑃 ∧ 𝑃 ⊆ 𝑈 ) )
5	1 2	lpiss	⊢ ( 𝑅 ∈ Ring → 𝑃 ⊆ 𝑈 )
6	5	biantrud	⊢ ( 𝑅 ∈ Ring → ( 𝑈 ⊆ 𝑃 ↔ ( 𝑈 ⊆ 𝑃 ∧ 𝑃 ⊆ 𝑈 ) ) )
7	4 6	bitr4id	⊢ ( 𝑅 ∈ Ring → ( 𝑈 = 𝑃 ↔ 𝑈 ⊆ 𝑃 ) )
8	7	pm5.32i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = 𝑃 ) ↔ ( 𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃 ) )
9	3 8	bitri	⊢ ( 𝑅 ∈ LPIR ↔ ( 𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃 ) )