Metamath Proof Explorer

Theorem gsumlsscl

Description: Closure of a group sum in a linear subspace: A (finitely supported) sum of scalar multiplications of vectors of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Hypotheses gsumlsscl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑀 )
gsumlsscl.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
gsumlsscl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion gsumlsscl ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) → ( ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ∈ 𝑍 ) )

Proof

Step Hyp Ref Expression
1 gsumlsscl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑀 )
2 gsumlsscl.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
3 gsumlsscl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
5 lmodabl ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Abel )
6 5 3ad2ant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) → 𝑀 ∈ Abel )
7 6 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) → 𝑀 ∈ Abel )
8 ssexg ⊢ ( ( 𝑉 ⊆ 𝑍 ∧ 𝑍 ∈ 𝑆 ) → 𝑉 ∈ V )
9 8 ancoms ⊢ ( ( 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) → 𝑉 ∈ V )
10 9 3adant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) → 𝑉 ∈ V )
11 10 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) → 𝑉 ∈ V )
12 3simpa ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) → ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ) )
13 1 lsssubg ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ) → 𝑍 ∈ ( SubGrp ‘ 𝑀 ) )
14 12 13 syl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) → 𝑍 ∈ ( SubGrp ‘ 𝑀 ) )
15 14 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) → 𝑍 ∈ ( SubGrp ‘ 𝑀 ) )
16 12 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) → ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ) )
17 16 adantr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ) )
18 elmapi ⊢ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) → 𝐹 : 𝑉 ⟶ 𝐵 )
19 ffvelrn ⊢ ( ( 𝐹 : 𝑉 ⟶ 𝐵 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝐵 )
20 19 ex ⊢ ( 𝐹 : 𝑉 ⟶ 𝐵 → ( 𝑣 ∈ 𝑉 → ( 𝐹 ‘ 𝑣 ) ∈ 𝐵 ) )
21 18 20 syl ⊢ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) → ( 𝑣 ∈ 𝑉 → ( 𝐹 ‘ 𝑣 ) ∈ 𝐵 ) )
22 21 ad2antrl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) → ( 𝑣 ∈ 𝑉 → ( 𝐹 ‘ 𝑣 ) ∈ 𝐵 ) )
23 22 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝐵 )
24 ssel ⊢ ( 𝑉 ⊆ 𝑍 → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝑍 ) )
25 24 3ad2ant3 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝑍 ) )
26 25 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝑍 ) )
27 26 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑍 )
28 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
29 2 28 3 1 lssvscl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ) ∧ ( ( 𝐹 ‘ 𝑣 ) ∈ 𝐵 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ∈ 𝑍 )
30 17 23 27 29 syl12anc ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ∈ 𝑍 )
31 30 fmpttd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) : 𝑉 ⟶ 𝑍 )
32 simp1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) → 𝑀 ∈ LMod )
33 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
34 33 1 lssss ⊢ ( 𝑍 ∈ 𝑆 → 𝑍 ⊆ ( Base ‘ 𝑀 ) )
35 sstr ⊢ ( ( 𝑉 ⊆ 𝑍 ∧ 𝑍 ⊆ ( Base ‘ 𝑀 ) ) → 𝑉 ⊆ ( Base ‘ 𝑀 ) )
36 35 expcom ⊢ ( 𝑍 ⊆ ( Base ‘ 𝑀 ) → ( 𝑉 ⊆ 𝑍 → 𝑉 ⊆ ( Base ‘ 𝑀 ) ) )
37 34 36 syl ⊢ ( 𝑍 ∈ 𝑆 → ( 𝑉 ⊆ 𝑍 → 𝑉 ⊆ ( Base ‘ 𝑀 ) ) )
38 37 a1i ⊢ ( 𝑀 ∈ LMod → ( 𝑍 ∈ 𝑆 → ( 𝑉 ⊆ 𝑍 → 𝑉 ⊆ ( Base ‘ 𝑀 ) ) ) )
39 38 3imp ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) → 𝑉 ⊆ ( Base ‘ 𝑀 ) )
40 elpwg ⊢ ( 𝑉 ∈ V → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ 𝑉 ⊆ ( Base ‘ 𝑀 ) ) )
41 10 40 syl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ 𝑉 ⊆ ( Base ‘ 𝑀 ) ) )
42 39 41 mpbird ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
43 32 42 jca ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
44 43 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
45 simprl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) → 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) )
46 simprr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) → 𝐹 finSupp ( 0g ‘ 𝑅 ) )
47 2 3 scmfsupp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) finSupp ( 0g ‘ 𝑀 ) )
48 44 45 46 47 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) finSupp ( 0g ‘ 𝑀 ) )
49 4 7 11 15 31 48 gsumsubgcl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ∈ 𝑍 )
50 49 ex ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍 ) → ( ( 𝐹 ∈ ( 𝐵 ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ 𝑅 ) ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ∈ 𝑍 ) )