Theorem mrclsp

Description: Moore closure generalizes module span. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypotheses	mrclsp.u	$$⊢U=\mathrm{LSubSp}\left(W\right)$$
	mrclsp.k	$$⊢K=\mathrm{LSpan}\left(W\right)$$
	mrclsp.f	$$⊢F=\mathrm{mrCls}\left(U\right)$$
Assertion	mrclsp	$$⊢W\in \mathrm{LMod}\to K=F$$

Proof

Step	Hyp	Ref	Expression
1		mrclsp.u	$$⊢U=\mathrm{LSubSp}\left(W\right)$$
2		mrclsp.k	$$⊢K=\mathrm{LSpan}\left(W\right)$$
3		mrclsp.f	$$⊢F=\mathrm{mrCls}\left(U\right)$$
4		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
5	4 1 2	lspfval	$$⊢W\in \mathrm{LMod}\to K=\left(a\in 𝒫{\mathrm{Base}}_W⟼\bigcap \left\{b\in U|a\subseteq b\right\}\right)$$
6	4 1	lssmre	$$⊢W\in \mathrm{LMod}\to U\in \mathrm{Moore}\left({\mathrm{Base}}_W\right)$$
7	3	mrcfval	$$⊢U\in \mathrm{Moore}\left({\mathrm{Base}}_W\right)\to F=\left(a\in 𝒫{\mathrm{Base}}_W⟼\bigcap \left\{b\in U|a\subseteq b\right\}\right)$$
8	6 7	syl	$$⊢W\in \mathrm{LMod}\to F=\left(a\in 𝒫{\mathrm{Base}}_W⟼\bigcap \left\{b\in U|a\subseteq b\right\}\right)$$
9	5 8	eqtr4d	$$⊢W\in \mathrm{LMod}\to K=F$$