Theorem elfilspd

Description: Simplified version of ellspd when the spanning set is finite: all linear combinations are then acceptable. (Contributed by Stefan O'Rear, 7-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

	Ref	Expression
Hypotheses	ellspd.n	|- N = ( LSpan ` M )
	ellspd.v	|- B = ( Base ` M )
	ellspd.k	|- K = ( Base ` S )
	ellspd.s	|- S = ( Scalar ` M )
	ellspd.z	|- .0. = ( 0g ` S )
	ellspd.t	|- .x. = ( .s ` M )
	elfilspd.f	|- ( ph -> F : I --> B )
	elfilspd.m	|- ( ph -> M e. LMod )
	elfilspd.i	|- ( ph -> I e. Fin )
Assertion	elfilspd	|- ( ph -> ( X e. ( N ` ( F " I ) ) <-> E. f e. ( K ^m I ) X = ( M gsum ( f oF .x. F ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ellspd.n	|- N = ( LSpan ` M )
2		ellspd.v	|- B = ( Base ` M )
3		ellspd.k	|- K = ( Base ` S )
4		ellspd.s	|- S = ( Scalar ` M )
5		ellspd.z	|- .0. = ( 0g ` S )
6		ellspd.t	|- .x. = ( .s ` M )
7		elfilspd.f	|- ( ph -> F : I --> B )
8		elfilspd.m	|- ( ph -> M e. LMod )
9		elfilspd.i	|- ( ph -> I e. Fin )
10	1 2 3 4 5 6 7 8 9	ellspd	|- ( ph -> ( X e. ( N ` ( F " I ) ) <-> E. f e. ( K ^m I ) ( f finSupp .0. /\ X = ( M gsum ( f oF .x. F ) ) ) ) )
11		elmapi	|- ( f e. ( K ^m I ) -> f : I --> K )
12	11	adantl	|- ( ( ph /\ f e. ( K ^m I ) ) -> f : I --> K )
13	9	adantr	|- ( ( ph /\ f e. ( K ^m I ) ) -> I e. Fin )
14	5	fvexi	|- .0. e. _V
15	14	a1i	|- ( ( ph /\ f e. ( K ^m I ) ) -> .0. e. _V )
16	12 13 15	fdmfifsupp	|- ( ( ph /\ f e. ( K ^m I ) ) -> f finSupp .0. )
17	16	biantrurd	|- ( ( ph /\ f e. ( K ^m I ) ) -> ( X = ( M gsum ( f oF .x. F ) ) <-> ( f finSupp .0. /\ X = ( M gsum ( f oF .x. F ) ) ) ) )
18	17	rexbidva	|- ( ph -> ( E. f e. ( K ^m I ) X = ( M gsum ( f oF .x. F ) ) <-> E. f e. ( K ^m I ) ( f finSupp .0. /\ X = ( M gsum ( f oF .x. F ) ) ) ) )
19	10 18	bitr4d	|- ( ph -> ( X e. ( N ` ( F " I ) ) <-> E. f e. ( K ^m I ) X = ( M gsum ( f oF .x. F ) ) ) )