Metamath Proof Explorer

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 ffvelrn ⊢ ( ( 𝐴 : 𝑉 ⟶ 𝑅 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑣 ) ∈ 𝑅 )
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 ffvelrn ⊢ ( ( 𝐴 : 𝑉 ⟶ 𝑅 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 )
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 ‘ 𝑀 ) 𝑉 ) )