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		ffvelcdm	⊢ ( ( 𝐹 : 𝑉 ⟶ 𝐵 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝐵 )
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 ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ∈ 𝑍 ) )