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

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 e. Ring -> ( I e. P <-> E. g e. 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 e. Ring -> P = U_ g e. B { ( K ` { g } ) } )
5 4 eleq2d 
 |-  ( R e. Ring -> ( I e. P <-> I e. U_ g e. B { ( K ` { g } ) } ) )
6 eliun 
 |-  ( I e. U_ g e. B { ( K ` { g } ) } <-> E. g e. B I e. { ( K ` { g } ) } )
7 fvex 
 |-  ( K ` { g } ) e. _V
8 7 elsn2 
 |-  ( I e. { ( K ` { g } ) } <-> I = ( K ` { g } ) )
9 8 rexbii 
 |-  ( E. g e. B I e. { ( K ` { g } ) } <-> E. g e. B I = ( K ` { g } ) )
10 6 9 bitri 
 |-  ( I e. U_ g e. B { ( K ` { g } ) } <-> E. g e. B I = ( K ` { g } ) )
11 5 10 bitrdi 
 |-  ( R e. Ring -> ( I e. P <-> E. g e. B I = ( K ` { g } ) ) )