Theorem lspfval

Description: The span function for a left vector space (or a left module). ( df-span analog.) (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lspval.v	|- V = ( Base ` W )
	lspval.s	|- S = ( LSubSp ` W )
	lspval.n	|- N = ( LSpan ` W )
Assertion	lspfval	|- ( W e. X -> N = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )

Proof

Step	Hyp	Ref	Expression
1		lspval.v	|- V = ( Base ` W )
2		lspval.s	|- S = ( LSubSp ` W )
3		lspval.n	|- N = ( LSpan ` W )
4		elex	|- ( W e. X -> W e. _V )
5		fveq2	|- ( w = W -> ( Base ` w ) = ( Base ` W ) )
6	5 1	eqtr4di	|- ( w = W -> ( Base ` w ) = V )
7	6	pweqd	|- ( w = W -> ~P ( Base ` w ) = ~P V )
8		fveq2	|- ( w = W -> ( LSubSp ` w ) = ( LSubSp ` W ) )
9	8 2	eqtr4di	|- ( w = W -> ( LSubSp ` w ) = S )
10	9	rabeqdv	|- ( w = W -> { t e. ( LSubSp ` w ) | s C_ t } = { t e. S | s C_ t } )
11	10	inteqd	|- ( w = W -> |^| { t e. ( LSubSp ` w ) | s C_ t } = |^| { t e. S | s C_ t } )
12	7 11	mpteq12dv	|- ( w = W -> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )
13		df-lsp	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
14	1	fvexi	|- V e. _V
15	14	pwex	|- ~P V e. _V
16	15	mptex	|- ( s e. ~P V |-> |^| { t e. S | s C_ t } ) e. _V
17	12 13 16	fvmpt	|- ( W e. _V -> ( LSpan ` W ) = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )
18	4 17	syl	|- ( W e. X -> ( LSpan ` W ) = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )
19	3 18	syl5eq	|- ( W e. X -> N = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )