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 biimpi ⊢ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
11 10 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
12 11 3ad2ant3 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
13 elpwg ⊢ ( 𝑉 ∈ 𝑊 → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ 𝑉 ⊆ ( Base ‘ 𝑀 ) ) )
14 1 a1i ⊢ ( 𝑉 ∈ 𝑊 → 𝐵 = ( Base ‘ 𝑀 ) )
15 14 eqcomd ⊢ ( 𝑉 ∈ 𝑊 → ( Base ‘ 𝑀 ) = 𝐵 )
16 15 sseq2d ⊢ ( 𝑉 ∈ 𝑊 → ( 𝑉 ⊆ ( Base ‘ 𝑀 ) ↔ 𝑉 ⊆ 𝐵 ) )
17 13 16 bitr2d ⊢ ( 𝑉 ∈ 𝑊 → ( 𝑉 ⊆ 𝐵 ↔ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
18 17 biimpa ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
19 18 3ad2ant2 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
20 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
21 5 12 19 20 syl3anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
22 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
23 lmodcmn ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ CMnd )
24 23 3ad2ant1 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝑀 ∈ CMnd )
25 simpl ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) → 𝑉 ∈ 𝑊 )
26 25 3ad2ant2 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝑉 ∈ 𝑊 )
27 5 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑀 ∈ LMod )
28 elmapi ⊢ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) → 𝐹 : 𝑉 ⟶ 𝑆 )
29 ffvelrn ⊢ ( ( 𝐹 : 𝑉 ⟶ 𝑆 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 )
30 29 ex ⊢ ( 𝐹 : 𝑉 ⟶ 𝑆 → ( 𝑣 ∈ 𝑉 → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 ) )
31 28 30 syl ⊢ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) → ( 𝑣 ∈ 𝑉 → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 ) )
32 31 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) → ( 𝑣 ∈ 𝑉 → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 ) )
33 32 3ad2ant3 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝑣 ∈ 𝑉 → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 ) )
34 33 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 )
35 ssel ⊢ ( 𝑉 ⊆ 𝐵 → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
36 35 adantl ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
37 36 3ad2ant2 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
38 37 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝐵 )
39 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
40 1 2 39 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ∈ 𝐵 )
41 27 34 38 40 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ∈ 𝐵 )
42 41 fmpttd ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) : 𝑉 ⟶ 𝐵 )
43 simpl ⊢ ( ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) → 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) )
44 43 3ad2ant3 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) )
45 simp3r ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝐹 finSupp 0 )
46 45 4 breqtrdi ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝐹 finSupp ( 0g ‘ 𝑅 ) )
47 2 3 scmfsupp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) finSupp ( 0g ‘ 𝑀 ) )
48 5 19 44 46 47 syl211anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) finSupp ( 0g ‘ 𝑀 ) )
49 1 22 24 26 42 48 gsumcl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ∈ 𝐵 )
50 21 49 eqeltrd ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )