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 ⊢ 𝐵 = ( Base ‘ 𝑀 )
linccl.r ⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
Assertion linccl ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑆 ( linC ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )

Proof

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