Theorem mrcrsp

Description: Moore closure generalizes ideal span. (Contributed by Stefan O'Rear, 4-Apr-2015)

	Ref	Expression
Hypotheses	mrcrsp.u	|- U = ( LIdeal ` R )
	mrcrsp.k	|- K = ( RSpan ` R )
	mrcrsp.f	|- F = ( mrCls ` U )
Assertion	mrcrsp	|- ( R e. Ring -> K = F )

Proof

Step	Hyp	Ref	Expression
1		mrcrsp.u	|- U = ( LIdeal ` R )
2		mrcrsp.k	|- K = ( RSpan ` R )
3		mrcrsp.f	|- F = ( mrCls ` U )
4		rlmlmod	|- ( R e. Ring -> ( ringLMod ` R ) e. LMod )
5		lidlval	|- ( LIdeal ` R ) = ( LSubSp ` ( ringLMod ` R ) )
6	1 5	eqtri	|- U = ( LSubSp ` ( ringLMod ` R ) )
7		rspval	|- ( RSpan ` R ) = ( LSpan ` ( ringLMod ` R ) )
8	2 7	eqtri	|- K = ( LSpan ` ( ringLMod ` R ) )
9	6 8 3	mrclsp	|- ( ( ringLMod ` R ) e. LMod -> K = F )
10	4 9	syl	|- ( R e. Ring -> K = F )