Metamath Proof Explorer

Theorem lincval

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

Ref Expression
Assertion lincval ⊢ M ∈ X ∧ S ∈ Base Scalar ⁡ M V ∧ V ∈ 𝒫 Base M → S linC ⁡ M V = ∑ M x ∈ V S ⁡ x ⋅ M x

Proof

Step Hyp Ref Expression
1 lincop ⊢ M ∈ X → linC ⁡ M = s ∈ Base Scalar ⁡ M v , v ∈ 𝒫 Base M ⟼ ∑ M x ∈ v s ⁡ x ⋅ M x
2 1 3ad2ant1 ⊢ M ∈ X ∧ S ∈ Base Scalar ⁡ M V ∧ V ∈ 𝒫 Base M → linC ⁡ M = s ∈ Base Scalar ⁡ M v , v ∈ 𝒫 Base M ⟼ ∑ M x ∈ v s ⁡ x ⋅ M x
3 2 oveqd ⊢ M ∈ X ∧ S ∈ Base Scalar ⁡ M V ∧ V ∈ 𝒫 Base M → S linC ⁡ M V = S s ∈ Base Scalar ⁡ M v , v ∈ 𝒫 Base M ⟼ ∑ M x ∈ v s ⁡ x ⋅ M x V
4 simp2 ⊢ M ∈ X ∧ S ∈ Base Scalar ⁡ M V ∧ V ∈ 𝒫 Base M → S ∈ Base Scalar ⁡ M V
5 simp3 ⊢ M ∈ X ∧ S ∈ Base Scalar ⁡ M V ∧ V ∈ 𝒫 Base M → V ∈ 𝒫 Base M
6 ovexd ⊢ M ∈ X ∧ S ∈ Base Scalar ⁡ M V ∧ V ∈ 𝒫 Base M → ∑ M x ∈ V S ⁡ x ⋅ M x ∈ V
7 simpr ⊢ s = S ∧ v = V → v = V
8 fveq1 ⊢ s = S → s ⁡ x = S ⁡ x
9 8 oveq1d ⊢ s = S → s ⁡ x ⋅ M x = S ⁡ x ⋅ M x
10 9 adantr ⊢ s = S ∧ v = V → s ⁡ x ⋅ M x = S ⁡ x ⋅ M x
11 7 10 mpteq12dv ⊢ s = S ∧ v = V → x ∈ v ⟼ s ⁡ x ⋅ M x = x ∈ V ⟼ S ⁡ x ⋅ M x
12 11 oveq2d ⊢ s = S ∧ v = V → ∑ M x ∈ v s ⁡ x ⋅ M x = ∑ M x ∈ V S ⁡ x ⋅ M x
13 oveq2 ⊢ v = V → Base Scalar ⁡ M v = Base Scalar ⁡ M V
14 eqid ⊢ s ∈ Base Scalar ⁡ M v , v ∈ 𝒫 Base M ⟼ ∑ M x ∈ v s ⁡ x ⋅ M x = s ∈ Base Scalar ⁡ M v , v ∈ 𝒫 Base M ⟼ ∑ M x ∈ v s ⁡ x ⋅ M x
15 12 13 14 ovmpox2 ⊢ S ∈ Base Scalar ⁡ M V ∧ V ∈ 𝒫 Base M ∧ ∑ M x ∈ V S ⁡ x ⋅ M x ∈ V → S s ∈ Base Scalar ⁡ M v , v ∈ 𝒫 Base M ⟼ ∑ M x ∈ v s ⁡ x ⋅ M x V = ∑ M x ∈ V S ⁡ x ⋅ M x
16 4 5 6 15 syl3anc ⊢ M ∈ X ∧ S ∈ Base Scalar ⁡ M V ∧ V ∈ 𝒫 Base M → S s ∈ Base Scalar ⁡ M v , v ∈ 𝒫 Base M ⟼ ∑ M x ∈ v s ⁡ x ⋅ M x V = ∑ M x ∈ V S ⁡ x ⋅ M x
17 3 16 eqtrd ⊢ M ∈ X ∧ S ∈ Base Scalar ⁡ M V ∧ V ∈ 𝒫 Base M → S linC ⁡ M V = ∑ M x ∈ V S ⁡ x ⋅ M x