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 P=LPIdealR
lpiss.u U=LIdealR
Assertion islpir RLPIRRRingU=P

Proof

Step Hyp Ref Expression
1 lpival.p P=LPIdealR
2 lpiss.u U=LIdealR
3 fveq2 r=RLIdealr=LIdealR
4 fveq2 r=RLPIdealr=LPIdealR
5 3 4 eqeq12d r=RLIdealr=LPIdealrLIdealR=LPIdealR
6 2 1 eqeq12i U=PLIdealR=LPIdealR
7 5 6 bitr4di r=RLIdealr=LPIdealrU=P
8 df-lpir LPIR=rRing|LIdealr=LPIdealr
9 7 8 elrab2 RLPIRRRingU=P