Metamath Proof Explorer

Theorem lincfsuppcl

Description: A linear combination of vectors (with finite support) is a vector. (Contributed by AV, 25-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Hypotheses lincfsuppcl.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
lincfsuppcl.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
lincfsuppcl.s ⊢ 𝑆 = ( Base ‘ 𝑅 )
lincfsuppcl.0 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion lincfsuppcl ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 lincfsuppcl.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 lincfsuppcl.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
3 lincfsuppcl.s ⊢ 𝑆 = ( Base ‘ 𝑅 )
4 lincfsuppcl.0 ⊢ 0 = ( 0g ‘ 𝑅 )
5 simp1 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝑀 ∈ LMod )
6 2 fveq2i ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
7 3 6 eqtri ⊢ 𝑆 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
8 7 oveq1i ⊢ ( 𝑆 ↑m 𝑉 ) = ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 )
9 8 eleq2i ⊢ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ↔ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
10 9 birani ⊢ ( ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
11 10 3ad2ant3 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
12 elpwg ⊢ ( 𝑉 ∈ 𝑊 → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ 𝑉 ⊆ ( Base ‘ 𝑀 ) ) )
13 1 a1i ⊢ ( 𝑉 ∈ 𝑊 → 𝐵 = ( Base ‘ 𝑀 ) )
14 13 eqcomd ⊢ ( 𝑉 ∈ 𝑊 → ( Base ‘ 𝑀 ) = 𝐵 )
15 14 sseq2d ⊢ ( 𝑉 ∈ 𝑊 → ( 𝑉 ⊆ ( Base ‘ 𝑀 ) ↔ 𝑉 ⊆ 𝐵 ) )
16 12 15 bitr2d ⊢ ( 𝑉 ∈ 𝑊 → ( 𝑉 ⊆ 𝐵 ↔ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
17 16 biimpa ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
18 17 3ad2ant2 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
19 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
20 5 11 18 19 syl3anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
21 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
22 lmodcmn ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ CMnd )
23 22 3ad2ant1 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝑀 ∈ CMnd )
24 simpl ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) → 𝑉 ∈ 𝑊 )
25 24 3ad2ant2 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝑉 ∈ 𝑊 )
26 5 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑀 ∈ LMod )
27 elmapi ⊢ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) → 𝐹 : 𝑉 ⟶ 𝑆 )
28 ffvelcdm ⊢ ( ( 𝐹 : 𝑉 ⟶ 𝑆 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 )
29 28 ex ⊢ ( 𝐹 : 𝑉 ⟶ 𝑆 → ( 𝑣 ∈ 𝑉 → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 ) )
30 27 29 syl ⊢ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) → ( 𝑣 ∈ 𝑉 → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 ) )
31 30 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) → ( 𝑣 ∈ 𝑉 → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 ) )
32 31 3ad2ant3 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝑣 ∈ 𝑉 → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 ) )
33 32 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 )
34 ssel ⊢ ( 𝑉 ⊆ 𝐵 → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
35 34 adantl ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
36 35 3ad2ant2 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
37 36 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝐵 )
38 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
39 1 2 38 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ∈ 𝐵 )
40 26 33 37 39 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ∈ 𝐵 )
41 40 fmpttd ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) : 𝑉 ⟶ 𝐵 )
42 simpl ⊢ ( ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) → 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) )
43 42 3ad2ant3 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) )
44 simp3r ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝐹 finSupp 0 )
45 44 4 breqtrdi ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝐹 finSupp ( 0g ‘ 𝑅 ) )
46 2 3 scmfsupp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) finSupp ( 0g ‘ 𝑀 ) )
47 5 18 43 45 46 syl211anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) finSupp ( 0g ‘ 𝑀 ) )
48 1 21 23 25 41 47 gsumcl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ∈ 𝐵 )
49 20 48 eqeltrd ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )