Theorem lpirring

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

	Ref	Expression
Assertion	lpirring	⊢ ( 𝑅 ∈ LPIR → 𝑅 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( LPIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 )
2		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
3	1 2	islpir	⊢ ( 𝑅 ∈ LPIR ↔ ( 𝑅 ∈ Ring ∧ ( LIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 ) ) )
4	3	simplbi	⊢ ( 𝑅 ∈ LPIR → 𝑅 ∈ Ring )