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	$⊢ S = LSubSp (M)$
	gsumlsscl.r	$⊢ R = Scalar (M)$
	gsumlsscl.b	$⊢ B = {Base}_{R}$
Assertion	gsumlsscl	$⊢ (M \in LMod \land Z \in S \land V \subseteq Z) \to ((F \in (B^{V}) \land {finSupp}_{0_{R}} (F)) \to \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v) \in Z)$

Proof

Step	Hyp	Ref	Expression
1		gsumlsscl.s	$⊢ S = LSubSp (M)$
2		gsumlsscl.r	$⊢ R = Scalar (M)$
3		gsumlsscl.b	$⊢ B = {Base}_{R}$
4		eqid	$⊢ 0_{M} = 0_{M}$
5		lmodabl	$⊢ M \in LMod \to M \in Abel$
6	5	3ad2ant1	$⊢ (M \in LMod \land Z \in S \land V \subseteq Z) \to M \in Abel$
7	6	adantr	$⊢ ((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \to M \in Abel$
8		ssexg	$⊢ (V \subseteq Z \land Z \in S) \to V \in V$
9	8	ancoms	$⊢ (Z \in S \land V \subseteq Z) \to V \in V$
10	9	3adant1	$⊢ (M \in LMod \land Z \in S \land V \subseteq Z) \to V \in V$
11	10	adantr	$⊢ ((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \to V \in V$
12		3simpa	$⊢ (M \in LMod \land Z \in S \land V \subseteq Z) \to (M \in LMod \land Z \in S)$
13	1	lsssubg	$⊢ (M \in LMod \land Z \in S) \to Z \in SubGrp (M)$
14	12 13	syl	$⊢ (M \in LMod \land Z \in S \land V \subseteq Z) \to Z \in SubGrp (M)$
15	14	adantr	$⊢ ((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \to Z \in SubGrp (M)$
16	12	adantr	$⊢ ((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \to (M \in LMod \land Z \in S)$
17	16	adantr	$⊢ (((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \land v \in V) \to (M \in LMod \land Z \in S)$
18		elmapi	$⊢ F \in (B^{V}) \to F : V ⟶ B$
19		ffvelcdm	$⊢ (F : V ⟶ B \land v \in V) \to F (v) \in B$
20	19	ex	$⊢ F : V ⟶ B \to (v \in V \to F (v) \in B)$
21	18 20	syl	$⊢ F \in (B^{V}) \to (v \in V \to F (v) \in B)$
22	21	ad2antrl	$⊢ ((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \to (v \in V \to F (v) \in B)$
23	22	imp	$⊢ (((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \land v \in V) \to F (v) \in B$
24		ssel	$⊢ V \subseteq Z \to (v \in V \to v \in Z)$
25	24	3ad2ant3	$⊢ (M \in LMod \land Z \in S \land V \subseteq Z) \to (v \in V \to v \in Z)$
26	25	adantr	$⊢ ((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \to (v \in V \to v \in Z)$
27	26	imp	$⊢ (((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \land v \in V) \to v \in Z$
28		eqid	$⊢ \cdot_{M} = \cdot_{M}$
29	2 28 3 1	lssvscl	$⊢ ((M \in LMod \land Z \in S) \land (F (v) \in B \land v \in Z)) \to F (v) \cdot_{M} v \in Z$
30	17 23 27 29	syl12anc	$⊢ (((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \land v \in V) \to F (v) \cdot_{M} v \in Z$
31	30	fmpttd	$⊢ ((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \to (v \in V ⟼ F (v) \cdot_{M} v) : V ⟶ Z$
32		simp1	$⊢ (M \in LMod \land Z \in S \land V \subseteq Z) \to M \in LMod$
33		eqid	$⊢ {Base}_{M} = {Base}_{M}$
34	33 1	lssss	$⊢ Z \in S \to Z \subseteq {Base}_{M}$
35		sstr	$⊢ (V \subseteq Z \land Z \subseteq {Base}_{M}) \to V \subseteq {Base}_{M}$
36	35	expcom	$⊢ Z \subseteq {Base}_{M} \to (V \subseteq Z \to V \subseteq {Base}_{M})$
37	34 36	syl	$⊢ Z \in S \to (V \subseteq Z \to V \subseteq {Base}_{M})$
38	37	a1i	$⊢ M \in LMod \to (Z \in S \to (V \subseteq Z \to V \subseteq {Base}_{M}))$
39	38	3imp	$⊢ (M \in LMod \land Z \in S \land V \subseteq Z) \to V \subseteq {Base}_{M}$
40		elpwg	$⊢ V \in V \to (V \in 𝒫 {Base}_{M} \leftrightarrow V \subseteq {Base}_{M})$
41	10 40	syl	$⊢ (M \in LMod \land Z \in S \land V \subseteq Z) \to (V \in 𝒫 {Base}_{M} \leftrightarrow V \subseteq {Base}_{M})$
42	39 41	mpbird	$⊢ (M \in LMod \land Z \in S \land V \subseteq Z) \to V \in 𝒫 {Base}_{M}$
43	32 42	jca	$⊢ (M \in LMod \land Z \in S \land V \subseteq Z) \to (M \in LMod \land V \in 𝒫 {Base}_{M})$
44	43	adantr	$⊢ ((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \to (M \in LMod \land V \in 𝒫 {Base}_{M})$
45		simprl	$⊢ ((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \to F \in (B^{V})$
46		simprr	$⊢ ((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \to {finSupp}_{0_{R}} (F)$
47	2 3	scmfsupp	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land F \in (B^{V}) \land {finSupp}_{0_{R}} (F)) \to {finSupp}_{0_{M}} ((v \in V ⟼ F (v) \cdot_{M} v))$
48	44 45 46 47	syl3anc	$⊢ ((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \to {finSupp}_{0_{M}} ((v \in V ⟼ F (v) \cdot_{M} v))$
49	4 7 11 15 31 48	gsumsubgcl	$⊢ ((M \in LMod \land Z \in S \land V \subseteq Z) \land (F \in (B^{V}) \land {finSupp}_{0_{R}} (F))) \to \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v) \in Z$
50	49	ex	$⊢ (M \in LMod \land Z \in S \land V \subseteq Z) \to ((F \in (B^{V}) \land {finSupp}_{0_{R}} (F)) \to \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v) \in Z)$

Metamath Proof Explorer

Theorem gsumlsscl

Proof