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 } ) ) )