Theorem linccl

Description: A linear combination of vectors is a vector. (Contributed by AV, 31-Mar-2019)

	Ref	Expression
Hypotheses	linccl.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	linccl.r	⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
Assertion	linccl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑆 ( linC ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		linccl.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		linccl.r	⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
3		simpl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝑀 ∈ LMod )
4	2	oveq1i	⊢ ( 𝑅 ↑m 𝑉 ) = ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 )
5	4	eleq2i	⊢ ( 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ↔ 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
6	5	biimpi	⊢ ( 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) → 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
7	6	3ad2ant3	⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
8	7	adantl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
9	1	sseq2i	⊢ ( 𝑉 ⊆ 𝐵 ↔ 𝑉 ⊆ ( Base ‘ 𝑀 ) )
10		fvex	⊢ ( Base ‘ 𝑀 ) ∈ V
11	10	ssex	⊢ ( 𝑉 ⊆ ( Base ‘ 𝑀 ) → 𝑉 ∈ V )
12		elpwg	⊢ ( 𝑉 ∈ V → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ 𝑉 ⊆ ( Base ‘ 𝑀 ) ) )
13	11 12	syl	⊢ ( 𝑉 ⊆ ( Base ‘ 𝑀 ) → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ 𝑉 ⊆ ( Base ‘ 𝑀 ) ) )
14	13	ibir	⊢ ( 𝑉 ⊆ ( Base ‘ 𝑀 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
15	9 14	sylbi	⊢ ( 𝑉 ⊆ 𝐵 → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
16	15	3ad2ant2	⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
17	16	adantl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
18		lincval	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑆 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
19	3 8 17 18	syl3anc	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑆 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
20		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
21		lmodcmn	⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ CMnd )
22	21	adantr	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝑀 ∈ CMnd )
23		simpr1	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝑉 ∈ Fin )
24	3	adantr	⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑀 ∈ LMod )
25	2	fvexi	⊢ 𝑅 ∈ V
26		elmapg	⊢ ( ( 𝑅 ∈ V ∧ 𝑉 ∈ Fin ) → ( 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ↔ 𝑆 : 𝑉 ⟶ 𝑅 ) )
27	25 26	mpan	⊢ ( 𝑉 ∈ Fin → ( 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ↔ 𝑆 : 𝑉 ⟶ 𝑅 ) )
28		ffvelcdm	⊢ ( ( 𝑆 : 𝑉 ⟶ 𝑅 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑆 ‘ 𝑣 ) ∈ 𝑅 )
29	28	ex	⊢ ( 𝑆 : 𝑉 ⟶ 𝑅 → ( 𝑣 ∈ 𝑉 → ( 𝑆 ‘ 𝑣 ) ∈ 𝑅 ) )
30	27 29	syl6bi	⊢ ( 𝑉 ∈ Fin → ( 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝑣 ∈ 𝑉 → ( 𝑆 ‘ 𝑣 ) ∈ 𝑅 ) ) )
31	30	imp	⊢ ( ( 𝑉 ∈ Fin ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑣 ∈ 𝑉 → ( 𝑆 ‘ 𝑣 ) ∈ 𝑅 ) )
32	31	3adant2	⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑣 ∈ 𝑉 → ( 𝑆 ‘ 𝑣 ) ∈ 𝑅 ) )
33	32	adantl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑣 ∈ 𝑉 → ( 𝑆 ‘ 𝑣 ) ∈ 𝑅 ) )
34	33	imp	⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑆 ‘ 𝑣 ) ∈ 𝑅 )
35		ssel	⊢ ( 𝑉 ⊆ 𝐵 → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
36	35	3ad2ant2	⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
37	36	adantl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
38	37	imp	⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝐵 )
39		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
40		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
41	1 39 40 2	lmodvscl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ‘ 𝑣 ) ∈ 𝑅 ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝑆 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ∈ 𝐵 )
42	24 34 38 41	syl3anc	⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ∈ 𝐵 )
43	42	fmpttd	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) : 𝑉 ⟶ 𝐵 )
44	16	anim2i	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
45		simpr3	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) )
46		elmapi	⊢ ( 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) → 𝑆 : 𝑉 ⟶ 𝑅 )
47	46	3ad2ant3	⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝑆 : 𝑉 ⟶ 𝑅 )
48	47	adantl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝑆 : 𝑉 ⟶ 𝑅 )
49		fvexd	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∈ V )
50	48 23 49	fdmfifsupp	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝑆 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
51	39 2	scmfsupp	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) finSupp ( 0g ‘ 𝑀 ) )
52	44 45 50 51	syl3anc	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) finSupp ( 0g ‘ 𝑀 ) )
53	1 20 22 23 43 52	gsumcl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ∈ 𝐵 )
54	19 53	eqeltrd	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑆 ( linC ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )