Theorem ellspd

Description: The elements of the span of an indexed collection of basic vectors are those vectors which can be written as finite linear combinations of basic vectors. (Contributed by Stefan O'Rear, 7-Feb-2015) (Revised by AV, 24-Jun-2019) (Revised by AV, 11-Apr-2024)

	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$$
	ellspd.f	$$⊢\phi \to F:I⟶B$$
	ellspd.m	$$⊢\phi \to M\in \mathrm{LMod}$$
	ellspd.i	$$⊢\phi \to I\in V$$
Assertion	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)$$

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		ellspd.f	$$⊢\phi \to F:I⟶B$$
8		ellspd.m	$$⊢\phi \to M\in \mathrm{LMod}$$
9		ellspd.i	$$⊢\phi \to I\in V$$
10		ffn	$$⊢F:I⟶B\to FFnI$$
11		fnima	$$⊢FFnI\to F\left[I\right]=\mathrm{ran}F$$
12	7 10 11	3syl	$$⊢\phi \to F\left[I\right]=\mathrm{ran}F$$
13	12	fveq2d	$$⊢\phi \to N\left(F\left[I\right]\right)=N\left(\mathrm{ran}F\right)$$
14		eqid	$$⊢\left(f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}⟼{\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right)=\left(f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}⟼{\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right)$$
15	14	rnmpt	$$⊢\mathrm{ran}\left(f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}⟼{\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right)=\left\{a|\exists f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}a={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right\}$$
16		eqid	$$⊢S\mathrm{freeLMod}I=S\mathrm{freeLMod}I$$
17		eqid	$$⊢{\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}$$
18	4	a1i	$$⊢\phi \to S=\mathrm{Scalar}\left(M\right)$$
19	16 17 2 6 14 8 9 18 7 1	frlmup3	$$⊢\phi \to \mathrm{ran}\left(f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}⟼{\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right)=N\left(\mathrm{ran}F\right)$$
20	15 19	eqtr3id	$$⊢\phi \to \left\{a|\exists f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}a={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right\}=N\left(\mathrm{ran}F\right)$$
21	13 20	eqtr4d	$$⊢\phi \to N\left(F\left[I\right]\right)=\left\{a|\exists f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}a={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right\}$$
22	21	eleq2d	$$⊢\phi \to \left(X\in N\left(F\left[I\right]\right)\leftrightarrow X\in \left\{a|\exists f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}a={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right\}\right)$$
23		ovex	$$⊢{\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\in \mathrm{V}$$
24		eleq1	$$⊢X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\to \left(X\in \mathrm{V}\leftrightarrow {\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\in \mathrm{V}\right)$$
25	23 24	mpbiri	$$⊢X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\to X\in \mathrm{V}$$
26	25	rexlimivw	$$⊢\exists f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\to X\in \mathrm{V}$$
27		eqeq1	$$⊢a=X\to \left(a={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\leftrightarrow X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right)$$
28	27	rexbidv	$$⊢a=X\to \left(\exists f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}a={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\leftrightarrow \exists f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right)$$
29	26 28	elab3	$$⊢X\in \left\{a|\exists f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}a={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right\}\leftrightarrow \exists f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)$$
30	4	fvexi	$$⊢S\in \mathrm{V}$$
31		eqid	$$⊢\left\{a\in \left(K^I\right)|{finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right\}=\left\{a\in \left(K^I\right)|{finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right\}$$
32	16 3 5 31	frlmbas	$$⊢\left(S\in \mathrm{V}\wedge I\in V\right)\to \left\{a\in \left(K^I\right)|{finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right\}={\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}$$
33	30 9 32	sylancr	$$⊢\phi \to \left\{a\in \left(K^I\right)|{finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right\}={\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}$$
34	33	eqcomd	$$⊢\phi \to {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}=\left\{a\in \left(K^I\right)|{finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right\}$$
35	34	rexeqdv	$$⊢\phi \to \left(\exists f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\leftrightarrow \exists f\in \left\{a\in \left(K^I\right)|{finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right\}X={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\right)\right)$$
36		breq1	$$⊢a=f\to \left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\leftrightarrow {finSupp}_{\underset{\dot{}}{0}}\left(f\right)\right)$$
37	36	rexrab	$$⊢\exists f\in \left\{a\in \left(K^I\right)|{finSupp}_{\underset{\dot{}}{0}}\left(a\right)\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)$$
38	35 37	bitrdi	$$⊢\phi \to \left(\exists f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}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)$$
39	29 38	bitrid	$$⊢\phi \to \left(X\in \left\{a|\exists f\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}a={\sum }_M\left(f{\underset{\dot{}}{·}}_{f}F\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)$$
40	22 39	bitrd	$$⊢\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)$$