Theorem lincop

Description: A linear combination as operation. (Contributed by AV, 30-Mar-2019)

	Ref	Expression
Assertion	lincop	$$⊢M\in X\to \mathrm{linC}\left(M\right)=\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_M⟼\underset{x\in v}{{\sum }_M}\left(s\left(x\right){\cdot }_{M}x\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{x\in v}{{\sum }_m}\left(s\left(x\right){\cdot }_{m}x\right)\right)\right)$$
2		2fveq3	$$⊢m=M\to {\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}$$
3	2	oveq1d	$$⊢m=M\to {{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v={{\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}}^v$$
4		fveq2	$$⊢m=M\to {\mathrm{Base}}_m={\mathrm{Base}}_M$$
5	4	pweqd	$$⊢m=M\to 𝒫{\mathrm{Base}}_m=𝒫{\mathrm{Base}}_M$$
6		id	$$⊢m=M\to m=M$$
7		fveq2	$$⊢m=M\to {\cdot }_m={\cdot }_M$$
8	7	oveqd	$$⊢m=M\to s\left(x\right){\cdot }_{m}x=s\left(x\right){\cdot }_{M}x$$
9	8	mpteq2dv	$$⊢m=M\to \left(x\in v⟼s\left(x\right){\cdot }_{m}x\right)=\left(x\in v⟼s\left(x\right){\cdot }_{M}x\right)$$
10	6 9	oveq12d	$$⊢m=M\to \underset{x\in v}{{\sum }_m}\left(s\left(x\right){\cdot }_{m}x\right)=\underset{x\in v}{{\sum }_M}\left(s\left(x\right){\cdot }_{M}x\right)$$
11	3 5 10	mpoeq123dv	$$⊢m=M\to \left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_m⟼\underset{x\in v}{{\sum }_m}\left(s\left(x\right){\cdot }_{m}x\right)\right)=\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_M⟼\underset{x\in v}{{\sum }_M}\left(s\left(x\right){\cdot }_{M}x\right)\right)$$
12		elex	$$⊢M\in X\to M\in \mathrm{V}$$
13		fvex	$$⊢{\mathrm{Base}}_M\in \mathrm{V}$$
14	13	pwex	$$⊢𝒫{\mathrm{Base}}_M\in \mathrm{V}$$
15		ovexd	$$⊢M\in X\to {{\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}}^v\in \mathrm{V}$$
16	15	ralrimivw	$$⊢M\in X\to \forall v\in 𝒫{\mathrm{Base}}_M{{\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}}^v\in \mathrm{V}$$
17		eqid	$$⊢\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_M⟼\underset{x\in v}{{\sum }_M}\left(s\left(x\right){\cdot }_{M}x\right)\right)=\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_M⟼\underset{x\in v}{{\sum }_M}\left(s\left(x\right){\cdot }_{M}x\right)\right)$$
18	17	mpoexxg2	$$⊢\left(𝒫{\mathrm{Base}}_M\in \mathrm{V}\wedge \forall v\in 𝒫{\mathrm{Base}}_M{{\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}}^v\in \mathrm{V}\right)\to \left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_M⟼\underset{x\in v}{{\sum }_M}\left(s\left(x\right){\cdot }_{M}x\right)\right)\in \mathrm{V}$$
19	14 16 18	sylancr	$$⊢M\in X\to \left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_M⟼\underset{x\in v}{{\sum }_M}\left(s\left(x\right){\cdot }_{M}x\right)\right)\in \mathrm{V}$$
20	1 11 12 19	fvmptd3	$$⊢M\in X\to \mathrm{linC}\left(M\right)=\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_M⟼\underset{x\in v}{{\sum }_M}\left(s\left(x\right){\cdot }_{M}x\right)\right)$$