Theorem lpi1

Description: The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lpival.p	|- P = ( LPIdeal ` R )
	lpi1.b	|- B = ( Base ` R )
Assertion	lpi1	|- ( R e. Ring -> B e. P )

Proof

Step	Hyp	Ref	Expression
1		lpival.p	|- P = ( LPIdeal ` R )
2		lpi1.b	|- B = ( Base ` R )
3		eqid	|- ( 1r ` R ) = ( 1r ` R )
4	2 3	ringidcl	|- ( R e. Ring -> ( 1r ` R ) e. B )
5		eqid	|- ( RSpan ` R ) = ( RSpan ` R )
6	5 2 3	rsp1	|- ( R e. Ring -> ( ( RSpan ` R ) ` { ( 1r ` R ) } ) = B )
7	6	eqcomd	|- ( R e. Ring -> B = ( ( RSpan ` R ) ` { ( 1r ` R ) } ) )
8		sneq	|- ( g = ( 1r ` R ) -> { g } = { ( 1r ` R ) } )
9	8	fveq2d	|- ( g = ( 1r ` R ) -> ( ( RSpan ` R ) ` { g } ) = ( ( RSpan ` R ) ` { ( 1r ` R ) } ) )
10	9	rspceeqv	|- ( ( ( 1r ` R ) e. B /\ B = ( ( RSpan ` R ) ` { ( 1r ` R ) } ) ) -> E. g e. B B = ( ( RSpan ` R ) ` { g } ) )
11	4 7 10	syl2anc	|- ( R e. Ring -> E. g e. B B = ( ( RSpan ` R ) ` { g } ) )
12	1 5 2	islpidl	|- ( R e. Ring -> ( B e. P <-> E. g e. B B = ( ( RSpan ` R ) ` { g } ) ) )
13	11 12	mpbird	|- ( R e. Ring -> B e. P )