This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑈 = 𝑃 ) )