Metamath Proof Explorer


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 )