Metamath Proof Explorer

Theorem lincop

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

Ref Expression
Assertion lincop ⊢M∈X→linC⁡M=s∈BaseScalar⁡Mv,v∈𝒫BaseM⟼∑Mx∈vs⁡x⋅Mx

Proof

Step Hyp Ref Expression
1 df-linc ⊢linC=m∈V⟼s∈BaseScalar⁡mv,v∈𝒫Basem⟼∑mx∈vs⁡x⋅mx
2 2fveq3 ⊢m=M→BaseScalar⁡m=BaseScalar⁡M
3 2 oveq1d ⊢m=M→BaseScalar⁡mv=BaseScalar⁡Mv
4 fveq2 ⊢m=M→Basem=BaseM
5 4 pweqd ⊢m=M→𝒫Basem=𝒫BaseM
6 id ⊢m=M→m=M
7 fveq2 ⊢m=M→⋅m=⋅M
8 7 oveqd ⊢m=M→s⁡x⋅mx=s⁡x⋅Mx
9 8 mpteq2dv ⊢m=M→x∈v⟼s⁡x⋅mx=x∈v⟼s⁡x⋅Mx
10 6 9 oveq12d ⊢m=M→∑mx∈vs⁡x⋅mx=∑Mx∈vs⁡x⋅Mx
11 3 5 10 mpoeq123dv ⊢m=M→s∈BaseScalar⁡mv,v∈𝒫Basem⟼∑mx∈vs⁡x⋅mx=s∈BaseScalar⁡Mv,v∈𝒫BaseM⟼∑Mx∈vs⁡x⋅Mx
12 elex ⊢M∈X→M∈V
13 fvex ⊢BaseM∈V
14 13 pwex ⊢𝒫BaseM∈V
15 ovexd ⊢M∈X→BaseScalar⁡Mv∈V
16 15 ralrimivw ⊢M∈X→∀v∈𝒫BaseMBaseScalar⁡Mv∈V
17 eqid ⊢s∈BaseScalar⁡Mv,v∈𝒫BaseM⟼∑Mx∈vs⁡x⋅Mx=s∈BaseScalar⁡Mv,v∈𝒫BaseM⟼∑Mx∈vs⁡x⋅Mx
18 17 mpoexxg2 ⊢𝒫BaseM∈V∧∀v∈𝒫BaseMBaseScalar⁡Mv∈V→s∈BaseScalar⁡Mv,v∈𝒫BaseM⟼∑Mx∈vs⁡x⋅Mx∈V
19 14 16 18 sylancr ⊢M∈X→s∈BaseScalar⁡Mv,v∈𝒫BaseM⟼∑Mx∈vs⁡x⋅Mx∈V
20 1 11 12 19 fvmptd3 ⊢M∈X→linC⁡M=s∈BaseScalar⁡Mv,v∈𝒫BaseM⟼∑Mx∈vs⁡x⋅Mx