Metamath Proof Explorer

Theorem dflinc2

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

Ref Expression
Assertion dflinc2 ⊢ linC = m ∈ V ⟼ s ∈ Base Scalar ⁡ m v , v ∈ 𝒫 Base m ⟼ ∑ m s ⋅ m f I ↾ v

Proof

Step Hyp Ref Expression
1 df-linc ⊢ linC = m ∈ V ⟼ s ∈ Base Scalar ⁡ m v , v ∈ 𝒫 Base m ⟼ ∑ m i ∈ v s ⁡ i ⋅ m i
2 elmapfn ⊢ s ∈ Base Scalar ⁡ m v → s Fn v
3 2 adantr ⊢ s ∈ Base Scalar ⁡ m v ∧ v ∈ 𝒫 Base m → s Fn v
4 fnresi ⊢ I ↾ v Fn v
5 4 a1i ⊢ s ∈ Base Scalar ⁡ m v ∧ v ∈ 𝒫 Base m → I ↾ v Fn v
6 vex ⊢ v ∈ V
7 6 a1i ⊢ s ∈ Base Scalar ⁡ m v ∧ v ∈ 𝒫 Base m → v ∈ V
8 inidm ⊢ v ∩ v = v
9 eqidd ⊢ s ∈ Base Scalar ⁡ m v ∧ v ∈ 𝒫 Base m ∧ i ∈ v → s ⁡ i = s ⁡ i
10 fvresi ⊢ i ∈ v → I ↾ v ⁡ i = i
11 10 adantl ⊢ s ∈ Base Scalar ⁡ m v ∧ v ∈ 𝒫 Base m ∧ i ∈ v → I ↾ v ⁡ i = i
12 3 5 7 7 8 9 11 offval ⊢ s ∈ Base Scalar ⁡ m v ∧ v ∈ 𝒫 Base m → s ⋅ m f I ↾ v = i ∈ v ⟼ s ⁡ i ⋅ m i
13 12 eqcomd ⊢ s ∈ Base Scalar ⁡ m v ∧ v ∈ 𝒫 Base m → i ∈ v ⟼ s ⁡ i ⋅ m i = s ⋅ m f I ↾ v
14 13 oveq2d ⊢ s ∈ Base Scalar ⁡ m v ∧ v ∈ 𝒫 Base m → ∑ m i ∈ v s ⁡ i ⋅ m i = ∑ m s ⋅ m f I ↾ v
15 14 mpoeq3ia ⊢ s ∈ Base Scalar ⁡ m v , v ∈ 𝒫 Base m ⟼ ∑ m i ∈ v s ⁡ i ⋅ m i = s ∈ Base Scalar ⁡ m v , v ∈ 𝒫 Base m ⟼ ∑ m s ⋅ m f I ↾ v
16 15 mpteq2i ⊢ m ∈ V ⟼ s ∈ Base Scalar ⁡ m v , v ∈ 𝒫 Base m ⟼ ∑ m i ∈ v s ⁡ i ⋅ m i = m ∈ V ⟼ s ∈ Base Scalar ⁡ m v , v ∈ 𝒫 Base m ⟼ ∑ m s ⋅ m f I ↾ v
17 1 16 eqtri ⊢ linC = m ∈ V ⟼ s ∈ Base Scalar ⁡ m v , v ∈ 𝒫 Base m ⟼ ∑ m s ⋅ m f I ↾ v