Theorem lincscm

Description: A linear combinations multiplied with a scalar is a linear combination, see also the proof in Lang p. 129. (Contributed by AV, 9-Apr-2019) (Revised by AV, 28-Jul-2019)

	Ref	Expression
Hypotheses	lincscm.s	⊢ ∙ = ( ·𝑠 ‘ 𝑀 )
	lincscm.t	⊢ · = ( .r ‘ ( Scalar ‘ 𝑀 ) )
	lincscm.x	⊢ 𝑋 = ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 )
	lincscm.r	⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
	lincscm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ ( 𝑆 · ( 𝐴 ‘ 𝑥 ) ) )
Assertion	lincscm	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑆 ∙ 𝑋 ) = ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		lincscm.s	⊢ ∙ = ( ·𝑠 ‘ 𝑀 )
2		lincscm.t	⊢ · = ( .r ‘ ( Scalar ‘ 𝑀 ) )
3		lincscm.x	⊢ 𝑋 = ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 )
4		lincscm.r	⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
5		lincscm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ ( 𝑆 · ( 𝐴 ‘ 𝑥 ) ) )
6		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
7		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
8		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
9		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
10		simp1l	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → 𝑀 ∈ LMod )
11		simpr	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
12	11	3ad2ant1	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
13		simpr	⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) → 𝑆 ∈ 𝑅 )
14	13	3ad2ant2	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → 𝑆 ∈ 𝑅 )
15	10	adantr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑀 ∈ LMod )
16		elmapi	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 : 𝑉 ⟶ 𝑅 )
17		ffvelcdm	⊢ ( ( 𝐴 : 𝑉 ⟶ 𝑅 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑣 ) ∈ 𝑅 )
18	17	ex	⊢ ( 𝐴 : 𝑉 ⟶ 𝑅 → ( 𝑣 ∈ 𝑉 → ( 𝐴 ‘ 𝑣 ) ∈ 𝑅 ) )
19	16 18	syl	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝑣 ∈ 𝑉 → ( 𝐴 ‘ 𝑣 ) ∈ 𝑅 ) )
20	19	adantr	⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) → ( 𝑣 ∈ 𝑉 → ( 𝐴 ‘ 𝑣 ) ∈ 𝑅 ) )
21	20	3ad2ant2	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑣 ∈ 𝑉 → ( 𝐴 ‘ 𝑣 ) ∈ 𝑅 ) )
22	21	imp	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑣 ) ∈ 𝑅 )
23		elelpwi	⊢ ( ( 𝑣 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑣 ∈ ( Base ‘ 𝑀 ) )
24	23	expcom	⊢ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ ( Base ‘ 𝑀 ) ) )
25	24	adantl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ ( Base ‘ 𝑀 ) ) )
26	25	3ad2ant1	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ ( Base ‘ 𝑀 ) ) )
27	26	imp	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ ( Base ‘ 𝑀 ) )
28		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
29	6 7 28 4	lmodvscl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐴 ‘ 𝑣 ) ∈ 𝑅 ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ∈ ( Base ‘ 𝑀 ) )
30	15 22 27 29	syl3anc	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ∈ ( Base ‘ 𝑀 ) )
31	7 4	scmfsupp	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) finSupp ( 0g ‘ 𝑀 ) )
32	31	3adant2r	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) finSupp ( 0g ‘ 𝑀 ) )
33	6 7 4 8 9 1 10 12 14 30 32	gsumvsmul	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( 𝑆 ∙ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ) = ( 𝑆 ∙ ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ) )
34	7	lmodring	⊢ ( 𝑀 ∈ LMod → ( Scalar ‘ 𝑀 ) ∈ Ring )
35	34	adantr	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( Scalar ‘ 𝑀 ) ∈ Ring )
36	35	3ad2ant1	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( Scalar ‘ 𝑀 ) ∈ Ring )
37	36	adantr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( Scalar ‘ 𝑀 ) ∈ Ring )
38	4	eleq2i	⊢ ( 𝑆 ∈ 𝑅 ↔ 𝑆 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
39	38	biimpi	⊢ ( 𝑆 ∈ 𝑅 → 𝑆 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
40	39	adantl	⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) → 𝑆 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
41	40	3ad2ant2	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → 𝑆 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
42	41	adantr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑆 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
43		ffvelcdm	⊢ ( ( 𝐴 : 𝑉 ⟶ 𝑅 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 )
44	43 4	eleqtrdi	⊢ ( ( 𝐴 : 𝑉 ⟶ 𝑅 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
45	44	ex	⊢ ( 𝐴 : 𝑉 ⟶ 𝑅 → ( 𝑥 ∈ 𝑉 → ( 𝐴 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
46	16 45	syl	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝑥 ∈ 𝑉 → ( 𝐴 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
47	46	adantr	⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) → ( 𝑥 ∈ 𝑉 → ( 𝐴 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
48	47	3ad2ant2	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑥 ∈ 𝑉 → ( 𝐴 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
49	48	imp	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
50		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
51	50 2	ringcl	⊢ ( ( ( Scalar ‘ 𝑀 ) ∈ Ring ∧ 𝑆 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐴 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑆 · ( 𝐴 ‘ 𝑥 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
52	37 42 49 51	syl3anc	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑆 · ( 𝐴 ‘ 𝑥 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
53	52 5	fmptd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
54		fvex	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V
55		elmapg	⊢ ( ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
56	54 12 55	sylancr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
57	53 56	mpbird	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
58		lincval	⊢ ( ( 𝑀 ∈ LMod ∧ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
59	10 57 12 58	syl3anc	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
60		simpr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
61		ovex	⊢ ( 𝑆 · ( 𝐴 ‘ 𝑣 ) ) ∈ V
62		fveq2	⊢ ( 𝑥 = 𝑣 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑣 ) )
63	62	oveq2d	⊢ ( 𝑥 = 𝑣 → ( 𝑆 · ( 𝐴 ‘ 𝑥 ) ) = ( 𝑆 · ( 𝐴 ‘ 𝑣 ) ) )
64	63 5	fvmptg	⊢ ( ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 · ( 𝐴 ‘ 𝑣 ) ) ∈ V ) → ( 𝐹 ‘ 𝑣 ) = ( 𝑆 · ( 𝐴 ‘ 𝑣 ) ) )
65	60 61 64	sylancl	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑣 ) = ( 𝑆 · ( 𝐴 ‘ 𝑣 ) ) )
66	65	oveq1d	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( ( 𝑆 · ( 𝐴 ‘ 𝑣 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
67	14	adantr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑆 ∈ 𝑅 )
68	6 7 28 4 2	lmodvsass	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ∈ 𝑅 ∧ ( 𝐴 ‘ 𝑣 ) ∈ 𝑅 ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝑆 · ( 𝐴 ‘ 𝑣 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 𝑆 ( ·𝑠 ‘ 𝑀 ) ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) )
69	15 67 22 27 68	syl13anc	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 · ( 𝐴 ‘ 𝑣 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 𝑆 ( ·𝑠 ‘ 𝑀 ) ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) )
70	1	eqcomi	⊢ ( ·𝑠 ‘ 𝑀 ) = ∙
71	70	a1i	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ·𝑠 ‘ 𝑀 ) = ∙ )
72	71	oveqd	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑆 ( ·𝑠 ‘ 𝑀 ) ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = ( 𝑆 ∙ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) )
73	69 72	eqtrd	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 · ( 𝐴 ‘ 𝑣 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 𝑆 ∙ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) )
74	66 73	eqtrd	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 𝑆 ∙ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) )
75	74	mpteq2dva	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = ( 𝑣 ∈ 𝑉 ↦ ( 𝑆 ∙ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
76	75	oveq2d	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( 𝑆 ∙ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ) )
77	59 76	eqtrd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( 𝑆 ∙ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ) )
78	3	a1i	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → 𝑋 = ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 ) )
79	4	oveq1i	⊢ ( 𝑅 ↑m 𝑉 ) = ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 )
80	79	eleq2i	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ↔ 𝐴 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
81	80	biimpi	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
82	81	adantr	⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) → 𝐴 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
83	82	3ad2ant2	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → 𝐴 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
84		lincval	⊢ ( ( 𝑀 ∈ LMod ∧ 𝐴 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
85	10 83 12 84	syl3anc	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
86	78 85	eqtrd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → 𝑋 = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
87	86	oveq2d	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑆 ∙ 𝑋 ) = ( 𝑆 ∙ ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ) )
88	33 77 87	3eqtr4rd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑆 ∈ 𝑅 ) ∧ 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑆 ∙ 𝑋 ) = ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) )