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	⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
	lpiss.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
Assertion	islpir	⊢ ( 𝑅 ∈ LPIR ↔ ( 𝑅 ∈ Ring ∧ 𝑈 = 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		lpival.p	⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
2		lpiss.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
3		fveq2	⊢ ( 𝑟 = 𝑅 → ( LIdeal ‘ 𝑟 ) = ( LIdeal ‘ 𝑅 ) )
4		fveq2	⊢ ( 𝑟 = 𝑅 → ( LPIdeal ‘ 𝑟 ) = ( LPIdeal ‘ 𝑅 ) )
5	3 4	eqeq12d	⊢ ( 𝑟 = 𝑅 → ( ( LIdeal ‘ 𝑟 ) = ( LPIdeal ‘ 𝑟 ) ↔ ( LIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 ) ) )
6	2 1	eqeq12i	⊢ ( 𝑈 = 𝑃 ↔ ( LIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 ) )
7	5 6	bitr4di	⊢ ( 𝑟 = 𝑅 → ( ( LIdeal ‘ 𝑟 ) = ( LPIdeal ‘ 𝑟 ) ↔ 𝑈 = 𝑃 ) )
8		df-lpir	⊢ LPIR = { 𝑟 ∈ Ring ∣ ( LIdeal ‘ 𝑟 ) = ( LPIdeal ‘ 𝑟 ) }
9	7 8	elrab2	⊢ ( 𝑅 ∈ LPIR ↔ ( 𝑅 ∈ Ring ∧ 𝑈 = 𝑃 ) )