Theorem mrcrsp

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

	Ref	Expression
Hypotheses	mrcrsp.u	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
	mrcrsp.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
	mrcrsp.f	$$⊢F=\mathrm{mrCls}\left(U\right)$$
Assertion	mrcrsp	$$⊢R\in \mathrm{Ring}\to K=F$$

Proof

Step	Hyp	Ref	Expression
1		mrcrsp.u	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
2		mrcrsp.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
3		mrcrsp.f	$$⊢F=\mathrm{mrCls}\left(U\right)$$
4		rlmlmod	$$⊢R\in \mathrm{Ring}\to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
5		lidlval	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)$$
6	1 5	eqtri	$$⊢U=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)$$
7		rspval	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
8	2 7	eqtri	$$⊢K=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
9	6 8 3	mrclsp	$$⊢\mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}\to K=F$$
10	4 9	syl	$$⊢R\in \mathrm{Ring}\to K=F$$