Theorem rsp0

Description: The span of the zero element is the zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	rspcl.k	|- K = ( RSpan ` R )
	rsp0.z	|- .0. = ( 0g ` R )
Assertion	rsp0	|- ( R e. Ring -> ( K ` { .0. } ) = { .0. } )

Proof

Step	Hyp	Ref	Expression
1		rspcl.k	|- K = ( RSpan ` R )
2		rsp0.z	|- .0. = ( 0g ` R )
3		rlmlmod	|- ( R e. Ring -> ( ringLMod ` R ) e. LMod )
4		rlm0	|- ( 0g ` R ) = ( 0g ` ( ringLMod ` R ) )
5	2 4	eqtri	|- .0. = ( 0g ` ( ringLMod ` R ) )
6		rspval	|- ( RSpan ` R ) = ( LSpan ` ( ringLMod ` R ) )
7	1 6	eqtri	|- K = ( LSpan ` ( ringLMod ` R ) )
8	5 7	lspsn0	|- ( ( ringLMod ` R ) e. LMod -> ( K ` { .0. } ) = { .0. } )
9	3 8	syl	|- ( R e. Ring -> ( K ` { .0. } ) = { .0. } )