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 )