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

Metamath Proof Explorer

Theorem lpi0

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

Ref Expression
Hypotheses lpival.p 
|- P = ( LPIdeal ` R )
lpi0.z 
|- .0. = ( 0g ` R )
Assertion lpi0 
|- ( R e. Ring -> { .0. } e. P )

Proof

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