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

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 )