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=\mathrm{LSpan}\left(M\right)$$
	ellspd.v	$$⊢B={\mathrm{Base}}_M$$
	ellspd.k	$$⊢K={\mathrm{Base}}_S$$
	ellspd.s	$$⊢S=\mathrm{Scalar}\left(M\right)$$
	ellspd.z	$$⊢\underset{\dot{}}{0}=0_S$$
	ellspd.t	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
	elfilspd.f	$$⊢\phi \to F:I⟶B$$
	elfilspd.m	$$⊢\phi \to M\in \mathrm{LMod}$$
	elfilspd.i	$$⊢\phi \to I\in \mathrm{Fin}$$
Assertion	elfilspd	$$⊢\phi \to \left(X\in N\left(F\left[I\right]\right)\leftrightarrow \exists f\in \left(K^I\right)X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ellspd.n	$$⊢N=\mathrm{LSpan}\left(M\right)$$
2		ellspd.v	$$⊢B={\mathrm{Base}}_M$$
3		ellspd.k	$$⊢K={\mathrm{Base}}_S$$
4		ellspd.s	$$⊢S=\mathrm{Scalar}\left(M\right)$$
5		ellspd.z	$$⊢\underset{\dot{}}{0}=0_S$$
6		ellspd.t	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
7		elfilspd.f	$$⊢\phi \to F:I⟶B$$
8		elfilspd.m	$$⊢\phi \to M\in \mathrm{LMod}$$
9		elfilspd.i	$$⊢\phi \to I\in \mathrm{Fin}$$
10	1 2 3 4 5 6 7 8 9	ellspd	$$⊢\phi \to \left(X\in N\left(F\left[I\right]\right)\leftrightarrow \exists f\in \left(K^I\right)\left({finSupp}_{\underset{\dot{}}{0}}\left(f\right)\wedge X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right)\right)$$
11		elmapi	$$⊢f\in \left(K^I\right)\to f:I⟶K$$
12	11	adantl	$$⊢\left(\phi \wedge f\in \left(K^I\right)\right)\to f:I⟶K$$
13	9	adantr	$$⊢\left(\phi \wedge f\in \left(K^I\right)\right)\to I\in \mathrm{Fin}$$
14	5	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
15	14	a1i	$$⊢\left(\phi \wedge f\in \left(K^I\right)\right)\to \underset{\dot{}}{0}\in \mathrm{V}$$
16	12 13 15	fdmfifsupp	$$⊢\left(\phi \wedge f\in \left(K^I\right)\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(f\right)$$
17	16	biantrurd	$$⊢\left(\phi \wedge f\in \left(K^I\right)\right)\to \left(X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\leftrightarrow \left({finSupp}_{\underset{\dot{}}{0}}\left(f\right)\wedge X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right)\right)$$
18	17	rexbidva	$$⊢\phi \to \left(\exists f\in \left(K^I\right)X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\leftrightarrow \exists f\in \left(K^I\right)\left({finSupp}_{\underset{\dot{}}{0}}\left(f\right)\wedge X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right)\right)$$
19	10 18	bitr4d	$$⊢\phi \to \left(X\in N\left(F\left[I\right]\right)\leftrightarrow \exists f\in \left(K^I\right)X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right)$$