Metamath Proof Explorer


Theorem islpidl

Description: Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lpival.p P = LPIdeal R
lpival.k K = RSpan R
lpival.b B = Base R
Assertion islpidl R Ring I P g B I = K g

Proof

Step Hyp Ref Expression
1 lpival.p P = LPIdeal R
2 lpival.k K = RSpan R
3 lpival.b B = Base R
4 1 2 3 lpival R Ring P = g B K g
5 4 eleq2d R Ring I P I g B K g
6 eliun I g B K g g B I K g
7 fvex K g V
8 7 elsn2 I K g I = K g
9 8 rexbii g B I K g g B I = K g
10 6 9 bitri I g B K g g B I = K g
11 5 10 bitrdi R Ring I P g B I = K g