Metamath Proof Explorer


Theorem lincval

Description: The value of a linear combination. (Contributed by AV, 30-Mar-2019)

Ref Expression
Assertion lincval MXSBaseScalarMVV𝒫BaseMSlinCMV=MxVSxMx

Proof

Step Hyp Ref Expression
1 lincop MXlinCM=sBaseScalarMv,v𝒫BaseMMxvsxMx
2 1 3ad2ant1 MXSBaseScalarMVV𝒫BaseMlinCM=sBaseScalarMv,v𝒫BaseMMxvsxMx
3 2 oveqd MXSBaseScalarMVV𝒫BaseMSlinCMV=SsBaseScalarMv,v𝒫BaseMMxvsxMxV
4 simp2 MXSBaseScalarMVV𝒫BaseMSBaseScalarMV
5 simp3 MXSBaseScalarMVV𝒫BaseMV𝒫BaseM
6 ovexd MXSBaseScalarMVV𝒫BaseMMxVSxMxV
7 simpr s=Sv=Vv=V
8 fveq1 s=Ssx=Sx
9 8 oveq1d s=SsxMx=SxMx
10 9 adantr s=Sv=VsxMx=SxMx
11 7 10 mpteq12dv s=Sv=VxvsxMx=xVSxMx
12 11 oveq2d s=Sv=VMxvsxMx=MxVSxMx
13 oveq2 v=VBaseScalarMv=BaseScalarMV
14 eqid sBaseScalarMv,v𝒫BaseMMxvsxMx=sBaseScalarMv,v𝒫BaseMMxvsxMx
15 12 13 14 ovmpox2 SBaseScalarMVV𝒫BaseMMxVSxMxVSsBaseScalarMv,v𝒫BaseMMxvsxMxV=MxVSxMx
16 4 5 6 15 syl3anc MXSBaseScalarMVV𝒫BaseMSsBaseScalarMv,v𝒫BaseMMxvsxMxV=MxVSxMx
17 3 16 eqtrd MXSBaseScalarMVV𝒫BaseMSlinCMV=MxVSxMx