Metamath Proof Explorer


Theorem lincscmcl

Description: The multiplication of a linear combination with a scalar is a linear combination, see also the proof in Lang p. 129. (Contributed by AV, 11-Apr-2019) (Proof shortened by AV, 28-Jul-2019)

Ref Expression
Hypotheses lincscmcl.s · ˙ = M
lincscmcl.r R = Base Scalar M
Assertion lincscmcl M LMod V 𝒫 Base M C R D M LinCo V C · ˙ D M LinCo V

Proof

Step Hyp Ref Expression
1 lincscmcl.s · ˙ = M
2 lincscmcl.r R = Base Scalar M
3 eqid Base M = Base M
4 eqid Scalar M = Scalar M
5 3 4 2 lcoval M LMod V 𝒫 Base M D M LinCo V D Base M x R V finSupp 0 Scalar M x D = x linC M V
6 5 adantr M LMod V 𝒫 Base M C R D M LinCo V D Base M x R V finSupp 0 Scalar M x D = x linC M V
7 simpl M LMod V 𝒫 Base M M LMod
8 7 ad2antrr M LMod V 𝒫 Base M C R D Base M x R V finSupp 0 Scalar M x D = x linC M V M LMod
9 simpr M LMod V 𝒫 Base M C R C R
10 9 adantr M LMod V 𝒫 Base M C R D Base M x R V finSupp 0 Scalar M x D = x linC M V C R
11 simprl M LMod V 𝒫 Base M C R D Base M x R V finSupp 0 Scalar M x D = x linC M V D Base M
12 3 4 1 2 lmodvscl M LMod C R D Base M C · ˙ D Base M
13 8 10 11 12 syl3anc M LMod V 𝒫 Base M C R D Base M x R V finSupp 0 Scalar M x D = x linC M V C · ˙ D Base M
14 4 lmodring M LMod Scalar M Ring
15 14 ad2antrr M LMod V 𝒫 Base M C R Scalar M Ring
16 15 adantl x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R Scalar M Ring
17 16 adantr x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R v V Scalar M Ring
18 9 adantl x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R C R
19 18 adantr x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R v V C R
20 elmapi x R V x : V R
21 ffvelrn x : V R v V x v R
22 21 ex x : V R v V x v R
23 20 22 syl x R V v V x v R
24 23 adantr x R V finSupp 0 Scalar M x D = x linC M V v V x v R
25 24 ad2antrr x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R v V x v R
26 25 imp x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R v V x v R
27 eqid Scalar M = Scalar M
28 2 27 ringcl Scalar M Ring C R x v R C Scalar M x v R
29 17 19 26 28 syl3anc x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R v V C Scalar M x v R
30 29 fmpttd x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R v V C Scalar M x v : V R
31 2 fvexi R V
32 simpr M LMod V 𝒫 Base M V 𝒫 Base M
33 32 adantr M LMod V 𝒫 Base M C R V 𝒫 Base M
34 33 adantl x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R V 𝒫 Base M
35 elmapg R V V 𝒫 Base M v V C Scalar M x v R V v V C Scalar M x v : V R
36 31 34 35 sylancr x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R v V C Scalar M x v R V v V C Scalar M x v : V R
37 30 36 mpbird x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R v V C Scalar M x v R V
38 15 33 9 3jca M LMod V 𝒫 Base M C R Scalar M Ring V 𝒫 Base M C R
39 38 adantl x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R Scalar M Ring V 𝒫 Base M C R
40 simpl x R V finSupp 0 Scalar M x D = x linC M V x R V
41 40 ad2antrr x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R x R V
42 simprl x R V finSupp 0 Scalar M x D = x linC M V finSupp 0 Scalar M x
43 42 ad2antrr x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R finSupp 0 Scalar M x
44 2 rmfsupp Scalar M Ring V 𝒫 Base M C R x R V finSupp 0 Scalar M x finSupp 0 Scalar M v V C Scalar M x v
45 39 41 43 44 syl3anc x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R finSupp 0 Scalar M v V C Scalar M x v
46 oveq2 D = x linC M V C · ˙ D = C · ˙ x linC M V
47 46 adantl finSupp 0 Scalar M x D = x linC M V C · ˙ D = C · ˙ x linC M V
48 47 adantl x R V finSupp 0 Scalar M x D = x linC M V C · ˙ D = C · ˙ x linC M V
49 48 ad2antrr x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R C · ˙ D = C · ˙ x linC M V
50 simprl x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R M LMod V 𝒫 Base M
51 40 adantr x R V finSupp 0 Scalar M x D = x linC M V D Base M x R V
52 51 9 anim12i x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R x R V C R
53 eqid x linC M V = x linC M V
54 eqid v V C Scalar M x v = v V C Scalar M x v
55 1 27 53 2 54 lincscm M LMod V 𝒫 Base M x R V C R finSupp 0 Scalar M x C · ˙ x linC M V = v V C Scalar M x v linC M V
56 50 52 43 55 syl3anc x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R C · ˙ x linC M V = v V C Scalar M x v linC M V
57 49 56 eqtrd x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R C · ˙ D = v V C Scalar M x v linC M V
58 breq1 s = v V C Scalar M x v finSupp 0 Scalar M s finSupp 0 Scalar M v V C Scalar M x v
59 oveq1 s = v V C Scalar M x v s linC M V = v V C Scalar M x v linC M V
60 59 eqeq2d s = v V C Scalar M x v C · ˙ D = s linC M V C · ˙ D = v V C Scalar M x v linC M V
61 58 60 anbi12d s = v V C Scalar M x v finSupp 0 Scalar M s C · ˙ D = s linC M V finSupp 0 Scalar M v V C Scalar M x v C · ˙ D = v V C Scalar M x v linC M V
62 61 rspcev v V C Scalar M x v R V finSupp 0 Scalar M v V C Scalar M x v C · ˙ D = v V C Scalar M x v linC M V s R V finSupp 0 Scalar M s C · ˙ D = s linC M V
63 37 45 57 62 syl12anc x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R s R V finSupp 0 Scalar M s C · ˙ D = s linC M V
64 63 ex x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R s R V finSupp 0 Scalar M s C · ˙ D = s linC M V
65 64 ex x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R s R V finSupp 0 Scalar M s C · ˙ D = s linC M V
66 65 rexlimiva x R V finSupp 0 Scalar M x D = x linC M V D Base M M LMod V 𝒫 Base M C R s R V finSupp 0 Scalar M s C · ˙ D = s linC M V
67 66 impcom D Base M x R V finSupp 0 Scalar M x D = x linC M V M LMod V 𝒫 Base M C R s R V finSupp 0 Scalar M s C · ˙ D = s linC M V
68 67 impcom M LMod V 𝒫 Base M C R D Base M x R V finSupp 0 Scalar M x D = x linC M V s R V finSupp 0 Scalar M s C · ˙ D = s linC M V
69 3 4 2 lcoval M LMod V 𝒫 Base M C · ˙ D M LinCo V C · ˙ D Base M s R V finSupp 0 Scalar M s C · ˙ D = s linC M V
70 69 ad2antrr M LMod V 𝒫 Base M C R D Base M x R V finSupp 0 Scalar M x D = x linC M V C · ˙ D M LinCo V C · ˙ D Base M s R V finSupp 0 Scalar M s C · ˙ D = s linC M V
71 13 68 70 mpbir2and M LMod V 𝒫 Base M C R D Base M x R V finSupp 0 Scalar M x D = x linC M V C · ˙ D M LinCo V
72 71 ex M LMod V 𝒫 Base M C R D Base M x R V finSupp 0 Scalar M x D = x linC M V C · ˙ D M LinCo V
73 6 72 sylbid M LMod V 𝒫 Base M C R D M LinCo V C · ˙ D M LinCo V
74 73 3impia M LMod V 𝒫 Base M C R D M LinCo V C · ˙ D M LinCo V