Theorem mrclsp

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

	Ref	Expression
Hypotheses	mrclsp.u	|- U = ( LSubSp ` W )
	mrclsp.k	|- K = ( LSpan ` W )
	mrclsp.f	|- F = ( mrCls ` U )
Assertion	mrclsp	|- ( W e. LMod -> K = F )

Proof

Step	Hyp	Ref	Expression
1		mrclsp.u	|- U = ( LSubSp ` W )
2		mrclsp.k	|- K = ( LSpan ` W )
3		mrclsp.f	|- F = ( mrCls ` U )
4		eqid	|- ( Base ` W ) = ( Base ` W )
5	4 1 2	lspfval	|- ( W e. LMod -> K = ( a e. ~P ( Base ` W ) |-> |^| { b e. U | a C_ b } ) )
6	4 1	lssmre	|- ( W e. LMod -> U e. ( Moore ` ( Base ` W ) ) )
7	3	mrcfval	|- ( U e. ( Moore ` ( Base ` W ) ) -> F = ( a e. ~P ( Base ` W ) |-> |^| { b e. U | a C_ b } ) )
8	6 7	syl	|- ( W e. LMod -> F = ( a e. ~P ( Base ` W ) |-> |^| { b e. U | a C_ b } ) )
9	5 8	eqtr4d	|- ( W e. LMod -> K = F )