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