Theorem dflinc2

Description: Alternative definition of linear combinations using the function operation. (Contributed by AV, 1-Apr-2019)

	Ref	Expression
Assertion	dflinc2	$$⊢\mathrm{linC}=\left(m\in \mathrm{V}⟼\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_m⟼{\sum }_m\left(s{{\cdot }_m}_f\left({\mathrm{I}\upharpoonright }_v\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-linc	$$⊢\mathrm{linC}=\left(m\in \mathrm{V}⟼\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_m⟼\underset{i\in v}{{\sum }_m}\left(s\left(i\right){\cdot }_{m}i\right)\right)\right)$$
2		elmapfn	$$⊢s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right)\to sFnv$$
3	2	adantr	$$⊢\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right)\wedge v\in 𝒫{\mathrm{Base}}_m\right)\to sFnv$$
4		fnresi	$$⊢\left({\mathrm{I}\upharpoonright }_v\right)Fnv$$
5	4	a1i	$$⊢\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right)\wedge v\in 𝒫{\mathrm{Base}}_m\right)\to \left({\mathrm{I}\upharpoonright }_v\right)Fnv$$
6		vex	$$⊢v\in \mathrm{V}$$
7	6	a1i	$$⊢\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right)\wedge v\in 𝒫{\mathrm{Base}}_m\right)\to v\in \mathrm{V}$$
8		inidm	$$⊢v\cap v=v$$
9		eqidd	$$⊢\left(\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right)\wedge v\in 𝒫{\mathrm{Base}}_m\right)\wedge i\in v\right)\to s\left(i\right)=s\left(i\right)$$
10		fvresi	$$⊢i\in v\to \left({\mathrm{I}\upharpoonright }_v\right)\left(i\right)=i$$
11	10	adantl	$$⊢\left(\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right)\wedge v\in 𝒫{\mathrm{Base}}_m\right)\wedge i\in v\right)\to \left({\mathrm{I}\upharpoonright }_v\right)\left(i\right)=i$$
12	3 5 7 7 8 9 11	offval	$$⊢\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right)\wedge v\in 𝒫{\mathrm{Base}}_m\right)\to s{{\cdot }_m}_f\left({\mathrm{I}\upharpoonright }_v\right)=\left(i\in v⟼s\left(i\right){\cdot }_{m}i\right)$$
13	12	eqcomd	$$⊢\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right)\wedge v\in 𝒫{\mathrm{Base}}_m\right)\to \left(i\in v⟼s\left(i\right){\cdot }_{m}i\right)=s{{\cdot }_m}_f\left({\mathrm{I}\upharpoonright }_v\right)$$
14	13	oveq2d	$$⊢\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right)\wedge v\in 𝒫{\mathrm{Base}}_m\right)\to \underset{i\in v}{{\sum }_m}\left(s\left(i\right){\cdot }_{m}i\right)={\sum }_m\left(s{{\cdot }_m}_f\left({\mathrm{I}\upharpoonright }_v\right)\right)$$
15	14	mpoeq3ia	$$⊢\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_m⟼\underset{i\in v}{{\sum }_m}\left(s\left(i\right){\cdot }_{m}i\right)\right)=\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_m⟼{\sum }_m\left(s{{\cdot }_m}_f\left({\mathrm{I}\upharpoonright }_v\right)\right)\right)$$
16	15	mpteq2i	$$⊢\left(m\in \mathrm{V}⟼\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_m⟼\underset{i\in v}{{\sum }_m}\left(s\left(i\right){\cdot }_{m}i\right)\right)\right)=\left(m\in \mathrm{V}⟼\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_m⟼{\sum }_m\left(s{{\cdot }_m}_f\left({\mathrm{I}\upharpoonright }_v\right)\right)\right)\right)$$
17	1 16	eqtri	$$⊢\mathrm{linC}=\left(m\in \mathrm{V}⟼\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_m⟼{\sum }_m\left(s{{\cdot }_m}_f\left({\mathrm{I}\upharpoonright }_v\right)\right)\right)\right)$$