Metamath Proof Explorer

Theorem linccl

Description: A linear combination of vectors is a vector. (Contributed by AV, 31-Mar-2019)

Ref Expression
Hypotheses linccl.b ⊢ B = Base M
linccl.r ⊢ R = Base Scalar ⁡ M
Assertion linccl ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → S linC ⁡ M V ∈ B

Proof

Step Hyp Ref Expression
1 linccl.b ⊢ B = Base M
2 linccl.r ⊢ R = Base Scalar ⁡ M
3 simpl ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → M ∈ LMod
4 2 oveq1i ⊢ R V = Base Scalar ⁡ M V
5 4 eleq2i ⊢ S ∈ R V ↔ S ∈ Base Scalar ⁡ M V
6 5 biimpi ⊢ S ∈ R V → S ∈ Base Scalar ⁡ M V
7 6 3ad2ant3 ⊢ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → S ∈ Base Scalar ⁡ M V
8 7 adantl ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → S ∈ Base Scalar ⁡ M V
9 1 sseq2i ⊢ V ⊆ B ↔ V ⊆ Base M
10 fvex ⊢ Base M ∈ V
11 10 ssex ⊢ V ⊆ Base M → V ∈ V
12 elpwg ⊢ V ∈ V → V ∈ 𝒫 Base M ↔ V ⊆ Base M
13 11 12 syl ⊢ V ⊆ Base M → V ∈ 𝒫 Base M ↔ V ⊆ Base M
14 13 ibir ⊢ V ⊆ Base M → V ∈ 𝒫 Base M
15 9 14 sylbi ⊢ V ⊆ B → V ∈ 𝒫 Base M
16 15 3ad2ant2 ⊢ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → V ∈ 𝒫 Base M
17 16 adantl ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → V ∈ 𝒫 Base M
18 lincval ⊢ M ∈ LMod ∧ S ∈ Base Scalar ⁡ M V ∧ V ∈ 𝒫 Base M → S linC ⁡ M V = ∑ M v ∈ V S ⁡ v ⋅ M v
19 3 8 17 18 syl3anc ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → S linC ⁡ M V = ∑ M v ∈ V S ⁡ v ⋅ M v
20 eqid ⊢ 0 M = 0 M
21 lmodcmn ⊢ M ∈ LMod → M ∈ CMnd
22 21 adantr ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → M ∈ CMnd
23 simpr1 ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → V ∈ Fin
24 3 adantr ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V ∧ v ∈ V → M ∈ LMod
25 2 fvexi ⊢ R ∈ V
26 elmapg ⊢ R ∈ V ∧ V ∈ Fin → S ∈ R V ↔ S : V ⟶ R
27 25 26 mpan ⊢ V ∈ Fin → S ∈ R V ↔ S : V ⟶ R
28 ffvelrn ⊢ S : V ⟶ R ∧ v ∈ V → S ⁡ v ∈ R
29 28 ex ⊢ S : V ⟶ R → v ∈ V → S ⁡ v ∈ R
30 27 29 syl6bi ⊢ V ∈ Fin → S ∈ R V → v ∈ V → S ⁡ v ∈ R
31 30 imp ⊢ V ∈ Fin ∧ S ∈ R V → v ∈ V → S ⁡ v ∈ R
32 31 3adant2 ⊢ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → v ∈ V → S ⁡ v ∈ R
33 32 adantl ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → v ∈ V → S ⁡ v ∈ R
34 33 imp ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V ∧ v ∈ V → S ⁡ v ∈ R
35 ssel ⊢ V ⊆ B → v ∈ V → v ∈ B
36 35 3ad2ant2 ⊢ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → v ∈ V → v ∈ B
37 36 adantl ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → v ∈ V → v ∈ B
38 37 imp ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V ∧ v ∈ V → v ∈ B
39 eqid ⊢ Scalar ⁡ M = Scalar ⁡ M
40 eqid ⊢ ⋅ M = ⋅ M
41 1 39 40 2 lmodvscl ⊢ M ∈ LMod ∧ S ⁡ v ∈ R ∧ v ∈ B → S ⁡ v ⋅ M v ∈ B
42 24 34 38 41 syl3anc ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V ∧ v ∈ V → S ⁡ v ⋅ M v ∈ B
43 42 fmpttd ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → v ∈ V ⟼ S ⁡ v ⋅ M v : V ⟶ B
44 16 anim2i ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → M ∈ LMod ∧ V ∈ 𝒫 Base M
45 simpr3 ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → S ∈ R V
46 elmapi ⊢ S ∈ R V → S : V ⟶ R
47 46 3ad2ant3 ⊢ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → S : V ⟶ R
48 47 adantl ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → S : V ⟶ R
49 fvexd ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → 0 Scalar ⁡ M ∈ V
50 48 23 49 fdmfifsupp ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → finSupp 0 Scalar ⁡ M ⁡ S
51 39 2 scmfsupp ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ S ∈ R V ∧ finSupp 0 Scalar ⁡ M ⁡ S → finSupp 0 M⁡ v ∈ V ⟼ S ⁡ v ⋅ M v
52 44 45 50 51 syl3anc ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → finSupp 0 M⁡ v ∈ V ⟼ S ⁡ v ⋅ M v
53 1 20 22 23 43 52 gsumcl ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → ∑ M v ∈ V S ⁡ v ⋅ M v ∈ B
54 19 53 eqeltrd ⊢ M ∈ LMod ∧ V ∈ Fin ∧ V ⊆ B ∧ S ∈ R V → S linC ⁡ M V ∈ B