Theorem lspval

Description: The span of a set of vectors (in a left module). ( spanval 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	lspval	|- ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) = |^| { t e. S | U 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	1 2 3	lspfval	|- ( W e. LMod -> N = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )
5	4	fveq1d	|- ( W e. LMod -> ( N ` U ) = ( ( s e. ~P V |-> |^| { t e. S | s C_ t } ) ` U ) )
6	5	adantr	|- ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) = ( ( s e. ~P V |-> |^| { t e. S | s C_ t } ) ` U ) )
7		eqid	|- ( s e. ~P V |-> |^| { t e. S | s C_ t } ) = ( s e. ~P V |-> |^| { t e. S | s C_ t } )
8		sseq1	|- ( s = U -> ( s C_ t <-> U C_ t ) )
9	8	rabbidv	|- ( s = U -> { t e. S | s C_ t } = { t e. S | U C_ t } )
10	9	inteqd	|- ( s = U -> |^| { t e. S | s C_ t } = |^| { t e. S | U C_ t } )
11		simpr	|- ( ( W e. LMod /\ U C_ V ) -> U C_ V )
12	1	fvexi	|- V e. _V
13	12	elpw2	|- ( U e. ~P V <-> U C_ V )
14	11 13	sylibr	|- ( ( W e. LMod /\ U C_ V ) -> U e. ~P V )
15	1 2	lss1	|- ( W e. LMod -> V e. S )
16		sseq2	|- ( t = V -> ( U C_ t <-> U C_ V ) )
17	16	rspcev	|- ( ( V e. S /\ U C_ V ) -> E. t e. S U C_ t )
18	15 17	sylan	|- ( ( W e. LMod /\ U C_ V ) -> E. t e. S U C_ t )
19		intexrab	|- ( E. t e. S U C_ t <-> |^| { t e. S | U C_ t } e. _V )
20	18 19	sylib	|- ( ( W e. LMod /\ U C_ V ) -> |^| { t e. S | U C_ t } e. _V )
21	7 10 14 20	fvmptd3	|- ( ( W e. LMod /\ U C_ V ) -> ( ( s e. ~P V |-> |^| { t e. S | s C_ t } ) ` U ) = |^| { t e. S | U C_ t } )
22	6 21	eqtrd	|- ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) = |^| { t e. S | U C_ t } )